- #ls_src * #rs_src #Hmid_src %2
- cases (comp_list … rs_src rs_dst) #xs * #rsi * #rsj * *
- #Hrs_src #Hrs_dst #Hneq
- %{ls_src} %{ls_dst} %{rsi} %{rsj} %{c_src} %{xs}
- #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
- lapply(Hcomp2 … Hmid_src Hmid_dst ?)
- [@(Hneq … Hend Hc_dst)]
- -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 //
- |@Hmid_src]
- |@Hmid_dst]
+ #ls_src * #rs_src #Hmid_src
+ cases (true_or_false (is_endc c_src)) #Hc_src
+ [ % % [ % % %{c_src} % // | @Hcomp1 % %{c_src} % // ]
+ | %2 cases (comp_list … rs_src rs_dst is_endc) #xs * #rsi * #rsj * * *
+ #Hrs_src #Hrs_dst #Hnotendc #Hneq
+ %{ls_src} %{ls_dst} %{rsi} %{rsj} %{c_src} %{xs}
+ #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_src]
+ |@Hmid_dst] ]