proposition: Lemma use_fresh {Σ} x : incl x Σ -> ~ In (fresh Σ) x.
proof: Proof. now intros H ? % H % fresh_spec. Qed.
imports: List Undecidability.StringRewriting.PCSnf Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions