#H lapply (H … (refl ??)) -H #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
(midtape ? lsb s0 (xs@ci::rs'')) src)
[ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
[ @Htb1
| #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ] ]
#H lapply (H … (refl ??)) -H #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
(midtape ? lsb s0 (xs@ci::rs'')) src)
[ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
[ @Htb1
| #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ] ]