- [ >(\P Hc0) @Hnotend @memb_hd | @Hnotendxs1 //]
- | *
- [ * #Hrsj #Hta %
- [ >Hta in Hc; >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- #Hc lapply (Hc ? (refl ??)) #Hendr1
- cut (xs = xs1)
- [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
- -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
- [ * normalize in ⊢ (%→?); //
- #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
- lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
- | #x2 #xs2 #IH *
- [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
- >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
- normalize in ⊢ (%→?); #H destruct (H)
- | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
- #Hnotendc #Hnotendcxs1 @eq_f @IH
- [ @(cons_injective_r … Heq)
- | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @memb_hd
- | @memb_cons @memb_cons // ]
- | #c #Hc @Hnotendcxs1 @memb_cons // ]
- ]
- ]
- | #Hxsxs1 >Hmid_dst >Hxsxs1 % ]
- | #rsj0 #c >Hrsj #Hrsj0 destruct (Hrsj0) ]
- | * #cj * #rs2 * #Hrs2 #Hta lapply (Hta ?)
- [ cases (Hneq … Hrs1) /2/ #H %2 @(H ?? Hrs2) ]
- -Hta #Hta >Hta in Hc; >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // #Hc lapply (Hc ? (refl ??)) #Hendr1
- (* lemmatize this proof *) cut (xs = xs1)
- [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
- -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
- [ * normalize in ⊢ (%→?); //
- #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
- lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
- | #x2 #xs2 #IH *
- [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
- >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
- normalize in ⊢ (%→?); #H destruct (H)
- | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
- #Hnotendc #Hnotendcxs1 @eq_f @IH
- [ @(cons_injective_r … Heq)
- | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @memb_hd
- | @memb_cons @memb_cons // ]
- | #c #Hc @Hnotendcxs1 @memb_cons // ]
- ]
+ [ >(\P Hc0) @Hnotend @memb_hd | @Hnotendxs1 //] ]
+ *
+ [ * #Hrsj >Hrsj #Hta % %2 >Hta >nth_change_vec // cases (reverse ? xs1) //
+ | * #cj * #rs2 * #Hrsj #Hta lapply (Hta ?)
+ [ cases (Hneq ?? Hrs1) /2/ #Hr1 %2 @(Hr1 ?? Hrsj) ] -Hta #Hta
+ %2 >Hta in Hc; whd in ⊢ (??%?→?);
+ change with (current ? (niltape ?)) in match (None ?);
+ <nth_vec_map >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ whd in ⊢ (??%?→?); #Hc cut (is_endc r1 = true)
+ [ cases (is_endc r1) in Hc; whd in ⊢ (??%?→?); //
+ change with (current ? (niltape ?)) in match (None ?);
+ <nth_vec_map >nth_change_vec // normalize #H destruct (H) ]
+ #Hendr1 cut (xs = xs1)
+ [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
+ -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
+ [ * normalize in ⊢ (%→?); //
+ #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
+ lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
+ | #x2 #xs2 #IH *
+ [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
+ >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
+ normalize in ⊢ (%→?); #H destruct (H)
+ | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
+ #Hnotendc #Hnotendcxs1 @eq_f @IH
+ [ @(cons_injective_r … Heq)
+ | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) @memb_hd
+ | @memb_cons @memb_cons // ]
+ | #c #Hc @Hnotendcxs1 @memb_cons // ]