Changeset 1480
 Timestamp:
 Nov 2, 2011, 1:59:17 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Integers.ma
r961 r1480 435 435 ∀x,y. eq x y = eq y x. 436 436 #x #y change with (eq_bv ??? = eq_bv ???) 437 @eq_bv_elim @eq_bv_elim /2/ 438 #E >E * #NE @False_ind @NE @refl 437 @eq_bv_elim @eq_bv_elim /2/ #H1 #H2 @⊥ [/2/  /2/] (*Andrea: XXX*) 439 438 qed. 440 439
Note: See TracChangeset
for help on using the changeset viewer.