proposition: Theorem PCP_U3: PCP ⪯ OU 3 X.
proof: Proof. exists PCP_to_U. intros C; split; auto using PCP_MU. rewrite OU_NOU; auto using MU_PCP. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)