proposition: Corollary PCP_U X: PCP ⪯ U X.
proof: Proof. eapply reduction_transitive. eapply PCP_U3. eapply unification_conserve; eauto. Qed.
imports: Undecidability.HOU(calculus.calculus concon.conservativity unification.higher_order_unification) Undecidability.HOU(third_order.pcp third_order.simplified third_order.huet)