proposition: Lemma MPCP_MPCP' c C: MPCP (c, C) <-> MPCP' (c, c::C).
proof: Proof. firstorder. 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)