Changeset 1014 for src/ASM/FoldStuff.ma


Ignore:
Timestamp:
Jun 21, 2011, 2:02:37 AM (9 years ago)
Author:
sacerdot
Message:

The main theorem is completely broken (again).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/FoldStuff.ma

    r990 r1014  
    2828coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    2929
    30 axiom VOID: Type[0].
     30(*axiom VOID: Type[0].
    3131axiom assert_false: VOID.
    3232definition bigbang: ∀A:Type[0].False → VOID → A.
     
    3434qed.
    3535
    36 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
     36coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
    3737
    3838lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
Note: See TracChangeset for help on using the changeset viewer.