proposition: Lemma hash_sig a : a el Sigma -> # <> a.
proof: Proof. intros; eapply fresh_spec. 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