proposition: Lemma rew_subset u v : u / v el R -> u / v el P.
proof: Proof. unfold P. intros. eauto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions Undecidability.Synthetic.Definitions