+lemma wsem_match_m : ∀src,dst,sig,n,is_startc,is_endc.
+src ≠ dst → src < S n → dst < S n →
+ match_m src dst sig n is_startc is_endc ⊫ R_match_m src dst sig n is_startc is_endc.
+#src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
+lapply (sem_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc Hdst) … Hloop) //
+-Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
+[ #tc whd in ⊢ (%→%); *
+ [ * * [ *
+ [ * #cur_src * #H1 #H2 #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #cj #rs0 #Hdiff #Hstartc #Hendc #Hnotend #Hnthi
+ @False_ind
+ >Hnthi in H1; whd in ⊢ (??%?→?); #H destruct (H) cases (Hdiff cur_src)
+ #Habs @Habs //
+ ]
+ | #Hci #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #cj #rs0 #Hdiff #Hstartc #Hendc #Hnotend
+ #Hnthi >Hnthi in Hci; normalize in ⊢ (%→?); #H destruct (H) ] ]
+ | #Hcj #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #cj #rs0 #Hdiff #Hstartc #Hendc #_ #_ #Hnthj >Hnthj in Hcj;
+ normalize in ⊢ (%→?); #H destruct (H) ]
+ ]
+ |* #ls * #ls0 * #rs * #rs0 * #x0 * #xs * * * #Hsrc #Hx0 #Hdst #H %
+ [>Hsrc *
+ [* [* #x * whd in ⊢ (??%?→?); #Habs destruct (Habs) >Hx0 #Habs destruct (Habs)
+ |whd in ⊢ (??%?→?); #Habs destruct (Habs) ]
+ |>Hdst whd in ⊢ (??%?→?); #Habs destruct (Habs) ]
+ |#ls1 #x1 #xs1 #ci #rsi #ls2 #x2 #rs2
+ #Hdiff #Hstart #Hend #Hnotend
+ >Hsrc #Hsrc1 destruct (Hsrc1) >Hdst #Hdst1 destruct (Hdst1)
+ %1 %{[ ]} %{rs0} normalize in ⊢ (%→?); #Heq #cj #l2 #Hl1
+ cut (xs=xs1)
+ [@(append_l1_injective_r … rs0 rs0 (refl …)) @(cons_injective_r …Heq)]
+ #eqxs <eqxs
+ whd in match (append ? [ ] (x2::xs)); >reverse_cons >associative_append
+ normalize in match (append ? [x2] ls2);
+ cases (H rsi l2 ci cj ? Hl1)
+ [* #_ #_ #H3 @H3
+ |>eqxs in e0; #e0 @(append_l2_injective … e0) //
+ ]
+ ]
+ ]
+|#tc #td #te #Hd #Hstar #IH #He lapply (IH He) -IH *
+ #IH1 #IH2 % [@IH1]
+
+
+ cases (comp_list ? (x1::xs1@ci::rsi) (x2::rs2) is_endc)
+ #l * #tl1 * #tl2 * * * #H1 #H2 #H3 #H4