proposition: Lemma correct1 x y : incl x Σ -> incl y Σ -> SR (R, x, y) -> PCSnf (R', x ++ [#], y ++ [#]).
proof: Proof. intros Hx Hy. cbn. induction 1 as [ | x' y']. - constructor. - inversion H as [ x y u v H1 H2 H3 ]; subst x' y'. simpl_list. eapply derv_trans. 1: eapply copy; eauto. simpl_list. econstructor. { econstructor. eapply in_app_iff. eauto. } simpl_list. eapply derv_trans. 1: eapply copy; eauto. simpl_list. econstructor. { econstructor. eapply in_app_iff. right. apply in_map_iff. eauto. } eapply IHrewt; [ | eauto]. eapply incl_app; [ eauto | ]. eapply incl_app; [ | eauto ]. unfold Σ. eauto. Qed.
imports: List Undecidability.StringRewriting.PCSnf Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions