Changeset 1367


Ignore:
Timestamp:
Oct 13, 2011, 5:48:09 PM (8 years ago)
Author:
sacerdot
Message:

Proof improvement, still somehow a bit slow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1353 r1367  
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    201 * *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H cases daemon (*Wilmer: XXX*) qed.
     201* #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct]
     202cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)]
     203%2 @nmk #abs -H H'; try (-H2 H2') destruct (abs) (*Wilmer: still slow destructs, why?*)
     204qed.
    202205
    203206lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
Note: See TracChangeset for help on using the changeset viewer.