proposition: Lemma reduction : SR ⪯ PCSnf.
proof: Proof. exists (fun '(R,x,y) => (R' R x y, x ++ fresh (Σ R x y), y ++ fresh (Σ R x y))). intros [[R x] y]. split. - eapply correct1; unfold Σ; eauto. - intros. eapply correct2 with (x0 := x) (y0 := y) (x1 := []) (y1 := []). 1-4: unfold Σ; eauto. now simpl_list. Qed.
imports: List Undecidability.StringRewriting.PCSnf Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions Undecidability.Synthetic.Definitions