Changeset 2121 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jun 27, 2012, 3:30:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2114 r2121 170 170 qed. 171 171 172 (*CSC: move elsewhere*) 172 173 lemma pair_replace: 173 174 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → … … 326 327 qed. 327 328 329 (*CSC: move elsewhere*) 328 330 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 329 331 #P #A #a #abs destruct … … 359 361 include alias "ASM/BitVectorTrie.ma". 360 362 363 (*CSC: move elsewhere*) 361 364 lemma jmpair_as_replace: 362 365 ∀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. … … 375 378 qed. 376 379 380 (*CSC: move elsewhere*) 377 381 lemma if_then_else_replace: 378 382 ∀T: Type[0]. … … 396 400 qed. 397 401 402 (*CSC: move elsewhere*) 398 403 lemma refl_to_jmrefl: 399 404 ∀a: Type[0].
Note: See TracChangeset
for help on using the changeset viewer.