proposition: Lemma P_inv c : c el P -> c = d \/ c = e \/ c el R \/ c = ( [#] / [#] ) \/ exists a, a el Sigma /\ c = [a] / [a].
proof: Proof. cbn. intros. firstorder. eapply in_app_iff in H. firstorder. eapply in_map_iff in H. firstorder. 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