Ignore:
Timestamp:
Jun 27, 2012, 3:30:58 PM (8 years ago)
Author:
sacerdot
Message:

More functions moved to the places they belong to

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2114 r2121  
    170170qed.
    171171
     172(*CSC: move elsewhere*)
    172173lemma pair_replace:
    173174 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
     
    326327qed.
    327328
     329(*CSC: move elsewhere*)
    328330lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    329331 #P #A #a #abs destruct
     
    359361include alias "ASM/BitVectorTrie.ma".
    360362
     363(*CSC: move elsewhere*)
    361364lemma jmpair_as_replace:
    362365 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
     
    375378qed.
    376379
     380(*CSC: move elsewhere*)
    377381lemma if_then_else_replace:
    378382  ∀T: Type[0].
     
    396400qed.
    397401
     402(*CSC: move elsewhere*)
    398403lemma refl_to_jmrefl:
    399404  ∀a: Type[0].
Note: See TracChangeset for help on using the changeset viewer.