Changeset 1516 for src/ASM/Vector.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r1330 r1516 60 60 ]) lt. 61 61 [ cases (not_le_Sn_O O) 62 normalize in absd1 62 normalize in absd1; 63 63 # H 64 64 cases (H absd1) 65 65  cases (not_le_Sn_O (S o)) 66 normalize in prf 66 normalize in prf; 67 67 # H 68 68 cases (H prf) 69 69  normalize 70 normalize in prf 70 normalize in prf; 71 71 @ le_S_S_to_le 72 72 assumption … … 474 474  S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 475 475 ] P v. 476 #A #n #P #v generalize in matchP cases v normalize //476 #A #n #P #v lapply P cases v normalize // 477 477 qed. 478 478 … … 487 487 normalize /2/ 488 488  #m #h #t #IH #y @(vector_inv_n … y) 489 #h' #t' #Ht #Hf whd in ⊢ (?%) 489 #h' #t' #Ht #Hf whd in ⊢ (?%); 490 490 @(f_elim ? h h') #Eh 491 491 [ @IH [ #Et @Ht >Eh >Et @refl  #NEt @Hf % #E' destruct (E') elim NEt /2/ ] … … 497 497 #A #f #f_true #n #v elim v 498 498 [ // 499  #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl499  #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl 500 500 ] qed. 501 501 … … 508 508 [ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl 509 509  #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t' 510 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/510 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/ 511 511 ] qed. 512 512
Note: See TracChangeset
for help on using the changeset viewer.