+ #Htd destruct (Htd) * #te * * * * >Hmidta_src >Hmidta_dst
+ cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
+ destruct (Hlsalsb)
+ [ <(reverse_reverse … ls) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 -H1 -H2 #_ #_ normalize in match (reverse ? [ ]); #Hte #_
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte) * * #_
+ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
+ cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst)
+ [@(eq_vec_change_vec … (niltape ?)) [@Htb1|@Htb2] ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H)] ]
+ normalize in match (left ??); normalize in match (right ??);
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons >associative_append #Hte
+ lapply (Hte ???? (refl ??) ? s0 ? (reverse ? tla) ?? (refl ??))
+ [ >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) // ] #Hte #_ #_ #_
+ * * #_ >Hte >nth_change_vec [|//] #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig tla)@s0::rs0)) (tail ? (reverse sig (reverse sig tla)@s0::rs0))) dst)
+ (midtape ? [ ] hdb (reverse sig (reverse sig tlb)@s::rs)) src)
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 //
+ | #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ]]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig tla))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ >length_reverse >length_reverse <(length_reverse ? ls) <Hlen'
+ >H1 normalize // ]
+ | #_ <(reverse_reverse … ls0) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #_ #_ #Hte
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
+ * * #_ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
+ cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst)
+ [ @(eq_vec_change_vec … (niltape ?)) // @Htb2 ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >current_mk_tape >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H) ]]
+ normalize in ⊢ (??%); <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte #_ #_
+ lapply (Hte s0 hdb (reverse ? tlb) rs0 ?
+ lsb s hda (reverse ? tla) rs ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte * * #_ >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig tlb)@s0::rs0)) (tail ? (reverse sig (reverse sig tlb)@s0::rs0))) dst)
+ (midtape ? lsb hda (reverse sig (reverse sig tla)@s::rs)) src)
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 %
+ | #j #Hj <Htb2 // >change_vec_commute [|@sym_not_eq //]
+ >nth_change_vec_neq in ⊢ (???%); // ]]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse ? (reverse ? tlb)) [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ normalize in ⊢ (??%); >length_append >reverse_reverse
+ <(length_reverse ? lsa) >Hlen' >H2 normalize //
+ ]
+ ]
+ ]
+ ]
+ ]