proposition: Lemma sep_doll : $ <> #.
proof: Proof. intros H. symmetry in H. now eapply fresh_spec in H. 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