Changeset 1937 for src/ASM/Util.ma


Ignore:
Timestamp:
May 11, 2012, 3:06:15 PM (8 years ago)
Author:
boender
Message:
  • filled in some of the gaps in the proof of Policy
  • reverted internal type of ppc_map from bool to jump_length (in order to help with termination)
  • moved some lemmas to Util
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1934 r1937  
    14231423 #A #a #b #EQ destruct //
    14241424qed.
     1425
     1426lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
     1427  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
     1428 #A #P #s1 #s2 / by /
     1429qed.
     1430
     1431lemma Some_eq:
     1432 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
     1433 #T #x #y #H @option_destruct_Some @H
     1434qed.
Note: See TracChangeset for help on using the changeset viewer.