Changeset 1512 for src/common


Ignore:
Timestamp:
Nov 17, 2011, 4:11:52 PM (8 years ago)
Author:
campbell
Message:

Shorten proof of goal that solves now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Integers.ma

    r1480 r1512  
    435435  ∀x,y. eq x y = eq y x.
    436436#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/
    438438qed.
    439439
Note: See TracChangeset for help on using the changeset viewer.