+ whd in ⊢ (%→?); #Hout >Hout >Htb whd
+ #ls #c_src #xs #end #rs #Hmid_src #Hnotend #Hend
+ lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
+ cases (current … (nth dst ? intape (niltape ?))) in Hcomp1;
+ [#Hcomp1 #_ %1 % [% | @Hcomp1 %2 %2 % ]
+ |#c_dst cases (true_or_false (c_src == c_dst)) #Hceq
+ [#_ #Hmid_dst cases (Hmid_dst c_dst (refl …)) -Hmid_dst
+ #ls_dst * #rs_dst #Hmid_dst %2
+ cases (comp_list … (xs@end::rs) rs_dst is_endc) #xs1 * #rsi * #rsj * * *
+ #Hrs_src #Hrs_dst #Hnotendc #Hneq
+ %{ls_dst} %{rsj} %
+ [<Hrs_dst >(\P Hceq) // ]]
+ #rsi0 #rsj0 #end #c #Hend #Hc_dst
+ >Hrs_src in Hmid_src; >Hend #Hmid_src
+ >Hrs_dst in Hmid_dst; >Hc_dst <(\P Hceq) #Hmid_dst
+ cut (is_endc end = true ∨ end ≠ c)
+ [cases (Hneq … Hend) /2/ -Hneq #Hneq %2 @(Hneq … Hc_dst) ] #Hneq
+ lapply (Hcomp2 … Hmid_src Hmid_dst ? Hneq)
+ [#c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) //
+ | @Hnotendc // ]
+ ]
+ -Hcomp2 #Hcomp2 <Hcomp2
+ % // % [
+ >Hcomp2 in Hc; >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // #H lapply (H ? (refl …))
+ cases (is_endc end) [|normalize #H destruct (H) ]
+ #_ % // #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) // | @Hnotendc // ]
+ |@Hmid_dst]
+ ]
+ |#_ #Hcomp1 #Hsrc cases (Hsrc ? (refl ??)) -Hsrc #ls * #rs #Hsrc
+ %1 %
+ [% % %{c_src} % // lapply (Hc c_src) -Hc >Hcomp1
+ [| %2 % % @(not_to_not ??? (\Pf Hceq)) #H destruct (H) // ]
+ cases (is_endc c_src) //
+ >Hsrc #Hc lapply (Hc (refl ??)) normalize #H destruct (H)
+ |@Hcomp1 %2 %1 %1 @(not_to_not ??? (\Pf Hceq)) #H destruct (H) //
+ ]
+ ]
+ ]
+ ]
+qed.
+
+#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb