+ [>append_nil #Hx1 <Hx1 in Hnotendx1; #Hnotendx1
+ lapply (Hnotendx1 end ?) [ @memb_append_l2 @memb_hd ]
+ >Hend #H destruct (H) ]
+ #ci -tl1 #tl1 #Hxs #H cases (H … (refl … )) -H
+ [ #Hendci % >Hrs0 in Hmid_dst; cut (ci = end ∧ x1 = xs)
+ [ lapply Hxs lapply Hnotendx1 lapply x1 elim xs in Hnotend;
+ [ #_ *
+ [ #_ normalize #H destruct (H) /2/
+ | #x2 #xs2 #Hnotendx2 normalize #H destruct (H)
+ >(Hnotendx2 ? (memb_hd …)) in Hend; #H destruct (H) ]
+ | #x2 #xs2 #IH #Hnotendx2 *
+ [ #_ normalize #H destruct (H) >(Hnotendx2 ci ?) in Hendci;
+ [ #H destruct (H)
+ | @memb_cons @memb_hd ]
+ | #x3 #xs3 #Hnotendx3 normalize #H destruct (H)
+ cases (IH … e0)
+ [ #H1 #H2 /2/
+ | #c0 #Hc0 @Hnotendx2 cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) @memb_hd
+ | @memb_cons @memb_cons @Hc0 ]
+ | #c0 #Hc0 @Hnotendx3 @memb_cons @Hc0 ]
+ ]
+ ]
+ | * #Hcieq #Hx1eq >Hx1eq #Hmid_dst
+ cases (Htrue ??????? (refl ??) Hmid_dst Hnotend)
+ <Hcieq >Hendci * #H destruct (H) ]
+ |cases tl2 in Hrs0;
+ [ >append_nil #Hrs0 destruct (Hrs0) * #Hcifalse#_ %2
+ cut (∃l.xs = x1@ci::l)
+ [lapply Hxs lapply Hnotendx1 lapply Hnotend lapply xs
+ -Hxs -xs -Hnotendx1 elim x1
+ [ *
+ [ #_ #_ normalize #H1 destruct (H1) >Hend in Hcifalse;
+ #H1 destruct (H1)
+ | #x2 #xs2 #_ #_ normalize #H >(cons_injective_l ????? H) %{xs2} % ]
+ | #x2 #xs2 #IHin *
+ [ #_ #Hnotendxs2 normalize #H destruct (H)
+ >(Hnotendxs2 ? (memb_hd …)) in Hend; #H destruct (H)
+ | #x3 #xs3 #Hnotendxs3 #Hnotendxs2 normalize #H destruct (H)
+ cases (IHin ??? e0)
+ [ #xs4 #Hxs4 >Hxs4 %{xs4} %
+ | #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) @Hnotendxs3 @memb_hd
+ | @Hnotendxs3 @memb_cons @memb_cons @Hc0 ]
+ | #c0 #Hc0 @Hnotendxs2 @memb_cons @Hc0 ]
+ ]
+ ]
+ ] * #l #Hxs' >Hxs'
+ #l0 #l1 % #H lapply (eq_f ?? (length ?) ?? H) -H
+ >length_append normalize >length_append >length_append
+ normalize >commutative_plus normalize #H destruct (H) -H
+ >associative_plus in e0; >associative_plus
+ >(plus_n_O (|x1|)) in ⊢(??%?→?); #H lapply (injective_plus_r … H)
+ -H normalize #H destruct (H)
+ | #cj #tl2' #Hrs0 * #Hcifalse #Hcomp
+ lapply (Htrue ls c x1 ci tl1 ls0 (cj::tl2') ???)
+ [ #c0 #Hc0 cases (orb_true_l … Hc0) #Hc0
+ [ @Hnotend >(\P Hc0) @memb_hd
+ | @Hnotendx1 // ]
+ | >Hmid_dst >Hrs0 %
+ | >Hxs %
+ | * * #_ #_ -Htrue #Htrue lapply (Htrue ?? (refl ??) ?) [ @(Hcomp ?? (refl ??)) ]
+ * #Htb >Htb #Hendci >Hrs0 >Hxs
+ cases (IH ls c xs end rs ? Hnotend Hend Hnotstart) -IH
+ [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ]
+ #_ #IH lapply Hxs lapply Hnotendx1 -Hxs -Hnotendx1 cases x1 in Hrs0;
+ [ #Hrs0 #_ whd in ⊢ (???%→?); #Hxs
+ cases (IH Hstart (c::ls0) cj tl2' ?)
+ [ -IH * #l * #l1 * #Hll1 #IH % %{(c::l)} %{l1}
+ % [ @eq_f @Hll1 ]
+ #cj0 #l2 #Hcj0 >(IH … Hcj0) >Htb
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq // ] @eq_f3 //
+ >reverse_cons >associative_append %
+ | #IH %2 #l #l1 >(?:l@c::xs@l1 = l@(c::xs)@l1) [|%]
+ @not_sub_list_merge
+ [ #l2 cut (∃xs'.xs = ci::xs')
+ [ cases xs in Hxs;
+ [ normalize #H destruct (H) >Hend in Hendci; #H destruct (H)
+ | #ci' #xs' normalize #H lapply (cons_injective_l ????? H)
+ #H1 >H1 %{xs'} % ]
+ ]
+ * #xs' #Hxs' >Hxs' normalize % #H destruct (H)
+ lapply (Hcomp … (refl ??)) * /2/
+ |#t #l2 #l3 % normalize #H lapply (cons_injective_r ????? H)
+ -H #H >H in IH; #IH cases (IH l2 l3) -IH #IH @IH % ]
+ | >Htb >nth_change_vec // >Hmid_dst >Hrs0 % ]
+ | #x2 #xs2 normalize in ⊢ (%→?); #Hrs0 #Hnotendxs2 normalize in ⊢ (%→?);
+ #Hxs cases (IH Hstart (c::ls0) x2 (xs2@cj::tl2') ?)
+ [ -IH * #l * #l1 * #Hll1 #IH % %{(c::l)} %{l1}
+ % [ @eq_f @Hll1 ]
+ #cj0 #l2 #Hcj0 >(IH … Hcj0) >Htb
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq // ] @eq_f3 //
+ >reverse_cons >associative_append %
+ | -IH #IH %2 #l #l1 >(?:l@c::xs@l1 = l@(c::xs)@l1) [|%]
+ @not_sub_list_merge_2 [| @IH]
+ cut (∃l2.xs = (x2::xs2)@ci::l2)
+ [lapply Hnotendxs2
+ lapply Hnotend -Hnotend lapply Hxs
+ >(?:x2::xs2@ci::tl1 = (x2::xs2)@ci::tl1) [|%]
+ lapply (x2::xs2) elim xs
+ [ *
+ [ normalize in ⊢ (%→?); #H1 destruct (H1)
+ >Hendci in Hend; #Hend destruct (Hend)
+ | #x3 #xs3 normalize in ⊢ (%→?); #H1 destruct (H1)
+ #_ #Hnotendx3 >(Hnotendx3 ? (memb_hd …)) in Hend;
+ #Hend destruct (Hend)
+ ]
+ | #x3 #xs3 #IHin *
+ [ normalize in ⊢ (%→?); #Hxs3 destruct (Hxs3) #_ #_
+ %{xs3} %
+ | #x4 #xs4 normalize in ⊢ (%→?); #Hxs3xs4 #Hnotend
+ #Hnotendxs4 destruct (Hxs3xs4) cases (IHin ? e0 ??)
+ [ #l0 #Hxs3 >Hxs3 %{l0} %
+ | #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) @memb_hd
+ | @memb_cons @memb_cons @Hc0 ]
+ | #c0 #Hc0 @Hnotendxs4 @memb_cons //
+ ]
+ ]
+ ]
+ ] * #l2 #Hxs'
+ >Hxs' #l3 normalize >associative_append normalize % #H
+ destruct (H) lapply (append_l2_injective ?????? e1) //
+ #H1 destruct (H1) cases (Hcomp ?? (refl ??)) /2/
+ | >Htb >nth_change_vec // >Hmid_dst >Hrs0 % ]
+ ]
+ ]
+ ]
+ ]
+ |lapply (\Pf eqx) -eqx #eqx >Hmid_dst #Htrue
+ cases (Htrue ? (refl ??) eqx) -Htrue #Htb #Hendcx #_
+ cases rs0 in Htb;
+ [ #_ %2 #l #l1 cases l
+ [ normalize cases xs
+ [ cases l1
+ [ normalize % #H destruct (H) cases eqx /2/
+ | #tmp1 #l2 normalize % #H destruct (H) ]
+ | #tmp1 #l2 normalize % #H destruct (H) ]
+ | #tmp1 #l2 normalize % #H destruct (H)cases l2 in e0;
+ [ normalize #H1 destruct (H1)
+ | #tmp2 #l3 normalize #H1 destruct (H1) ]
+ ]
+ | #r1 #rs1 normalize in ⊢ (???(????%?)→?); #Htb >Htb in IH; #IH
+ cases (IH ls x xs end rs ? Hnotend Hend Hnotstart)
+ [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ] -IH
+ #_ #IH cases (IH Hstart (c::ls0) r1 rs1 ?)
+ [|| >nth_change_vec // ] -IH
+ [ * #l * #l1 * #Hll1 #Hout % %{(c::l)} %{l1} % >Hll1 //
+ >reverse_cons >associative_append #cj0 #ls #Hl1 >(Hout ?? Hl1)
+ >change_vec_commute in ⊢ (??(???%??)?); // @sym_not_eq //
+ | #IH %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@IH]
+ #l1 % #H destruct (H) cases eqx /2/