- #_ #Htrue cases (comp_list ? (xs@end::rs) rs0 is_endc)
- #x1 * #tl1 * #tl2 * * * #Hxs #Hrs0 #Hnotendx1
- cases tl1 in Hxs;
- [>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 % ]
- ]
- ]
+ #Htrue cases (Htrue (refl ??)) -Htrue
+ #xs0 * #ci * #rs' * #ls1 * #cj * #rs1 * * #Hxs #H destruct (H) #Hcicj
+ >Htc in IH; whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+ #IH cases (IH … Hmidta_src) -IH #_ >nth_change_vec //
+ cut (∃x1,xs1.xs0@cj::rs1 = x1::xs1)
+ [ cases xs0 [ %{cj} %{rs1} % | #x1 #xs1 %{x1} %{(xs1@cj::rs1)} % ] ] * #x1 * #xs1
+ #Hxs1 >Hxs1 #IH cases (IH … (refl ??)) -IH
+ [ * #l * #l1 * #Hxs1'
+ >change_vec_commute // >change_vec_change_vec
+ #Houtc % %{(c::l)} %{l1} %
+ [ normalize <Hxs1' %
+ | >reverse_cons >associative_append >change_vec_commute // @Houtc ]
+ | #H %2 #l #l1 >(?:l@c::xs@l1 = l@(c::xs)@l1) [|%]
+ @not_sub_list_merge
+ [ #l2 >Hxs <Hxs1 % normalize #H1 lapply (cons_injective_r ????? H1)
+ >associative_append #H2 lapply (append_l2_injective ????? (refl ??) H2)
+ #H3 lapply (cons_injective_l ????? H3) #H3 >H3 in Hcicj; * /2/
+ |#t #l2 #l3 % normalize #H1 lapply (cons_injective_r ????? H1)
+ -H1 #H1 cases (H l2 l3) #H2 @H2 @H1