proposition: Lemma MPCP_U3 X: MPCP ⪯ OU 3 X.
proof: Proof. exists (fun '(c, C) => MPCP'_to_U X (c, c::C)). intros [c C]; rewrite MPCP_MPCP'; split. all: eauto using MPCP'_U3, U3_MPCP'. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)