proposition: Lemma copy u v : incl u Σ -> derv R' (u ++ v) (v ++ u).
proof: Proof. intros Hu. induction u in v, Hu |- *; cbn. - simpl_list. constructor. - replace (a :: u ++ v) with ([a] ++ (u ++ v)) by reflexivity. replace (v ++ rev u ++ [a]) with ((v ++ rev u) ++ [a]) by now simpl_list. econstructor. constructor. eapply in_app_iff. right. eapply in_map_iff. eauto. simpl_list. replace (v ++ a :: u) with ((v ++ [a]) ++ u) by now simpl_list. eapply IHu. eapply incl_cons_inv. eassumption. Qed.
imports: List Undecidability.StringRewriting.PCSnf Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions