Changeset 1934 for src/ASM/Util.ma


Ignore:
Timestamp:
May 10, 2012, 3:37:07 PM (9 years ago)
Author:
boender
Message:
  • various & sundry moves of lemmas to better places
  • integrated Policy and Assembly
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1928 r1934  
    14131413  | #hd #tl #IH #l2 normalize <IH //]
    14141414qed.
     1415
     1416lemma nth_cons:
     1417  ∀n,A,h,t,y.
     1418  nth (S n) A (h::t) y = nth n A t y.
     1419 #n #A #h #t #y /2 by refl/
     1420qed.
     1421
     1422lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
     1423 #A #a #b #EQ destruct //
     1424qed.
Note: See TracChangeset for help on using the changeset viewer.