proposition: Lemma MPCP'_U3 P: MPCP' P -> OU 3 X (MPCP'_to_U P).
proof: Proof. destruct P as [c C]; intros (I & Sub & EQ). exists [alpha]. exists (finst I (length C) .: var); split. - intros x A. destruct x as [| [|]]; try discriminate; cbn. injection 1 as ?; subst. eapply finst_typing; eauto. - cbn -[enc]. rewrite !enc_subst_id; trivial. rewrite !AppR_subst, !Enc_subst_id; trivial. cbn; rewrite !ren_plus_base, !ren_plus_combine; change (1 + 1) with 2. erewrite <-map_length at 1. symmetry. erewrite <-map_length at 1. erewrite !finst_equivalence. all: simplify; trivial. now rewrite <-!enc_app, EQ. 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)