Changeset 1516 for src/ASM/Util.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r1323 r1516 219 219 #ABSURD 220 220 elim (ABSURD nil_absurd) 221 | normalize in cons_proof 221 | normalize in cons_proof; 222 222 @le_S_S_to_le 223 223 assumption … … 275 275 | 3: normalize 276 276 generalize in match (sig2 … (reduce_strong A B tl tl1)); 277 >p2 >p3 >p4 normalize in ⊢ (% → ?) 277 >p2 >p3 >p4 normalize in ⊢ (% → ?); 278 278 #HYP // 279 279 ] … … 377 377 ∀a:A. 378 378 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 379 #A #a #P #H #x #p 380 generalize in match H 381 generalize in match P 382 cases p 383 // 379 #A #a #P #H #x #p lapply H lapply P cases p // 384 380 qed. 385 381 … … 400 396 @ p 401 397 | 4: 402 normalize in prf2 398 normalize in prf2; 403 399 normalize 404 400 @ le_S_S_to_le … … 562 558 #A #B #H #acc #suff elim suff 563 559 [ #pre >append_nil % 564 | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]560 | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ] 565 561 qed. 566 562
Note: See TracChangeset
for help on using the changeset viewer.