Changeset 961 for src/common/Integers.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Integers.ma
r889 r961 436 436 #x #y change with (eq_bv ??? = eq_bv ???) 437 437 @eq_bv_elim @eq_bv_elim /2/ 438 [ #NE #E @False_ind >E in NE * /2/ 439  #E #NE @False_ind >E in NE * /2/ 440 ] qed. 438 #E >E * #NE @False_ind @NE @refl 439 qed. 441 440 442 441 theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
Note: See TracChangeset
for help on using the changeset viewer.