proposition: Lemma pequiv_equiv : RelationClasses.Equivalence pequiv.
proof: Proof. Proof using HE1 HE2 HE3. split. - intros [x y]. split; now apply HE1. - intros [x1 y1] [x2 y2] [H1 H2]; split; now apply HE2. - intros [x1 y1] [x2 y2] [x3 y3] [Hx1 Hx2] [Hy1 Hy2]; split; [eapply HE3 with x2 | eapply HE3 with y2]; easy. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation