 Timestamp:
 May 22, 2012, 12:57:17 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1978 r1979 142 142 1: 143 143 #A #B #T #P #a #b 144 #c #c' #t #EQc >EQc in t; c' #f #EQ normalize lapply f lapply EQ EQ f cases c 145 cases daemon (* CSC: extremely difficult to prove... 146 normalize #a' #b' @(pose … 〈a,b〉) #H #f 147 @(pose … 〈a,b〉) 148 @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) H)) ?? H) 149 check(E ????? H) 150 cut (a=a' ∧ b=b') 151 [ destruct /2/ 152  * #EQa #EQb >EQa in H; >EQb #H check (E ????? H) 153 #H cut (a=a') [2: #Eqa >Eqa in H; #H 154 155 156 * #x #y * #x' #y' #t #H1 #H2 cases H1 in H2; normalize 157 #X H1 destruct(X) destruct // 158 ]*) 144 #c #c' #t #EQc >EQc in t; c' normalize #f #EQ 145 letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ] 146 change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ; 147 @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize eta 148 EQ cases c in f; normalize // 149 ] 159 150 qed. 160 151
Note: See TracChangeset
for help on using the changeset viewer.