Changeset 1512 for src/common/Integers.ma
 Timestamp:
 Nov 17, 2011, 4:11:52 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Integers.ma
r1480 r1512 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/ #H1 #H2 @⊥ [/2/  /2/] (*Andrea: XXX*)437 @eq_bv_elim @eq_bv_elim /2/ 438 438 qed. 439 439
Note: See TracChangeset
for help on using the changeset viewer.