proposition: Lemma U3_MPCP' P: OU 3 X (MPCP'_to_U P) -> MPCP' P.
proof: Proof. destruct P as [c C]. intros (Delta & sigma & T1 & EQ). specialize (T1 0 (Arr (repeat (alpha → alpha) (length C)) alpha)); mp T1; trivial. eapply ordertyping_preservation_under_renaming with (delta := add 2) (Delta := alpha :: alpha :: Delta) in T1. 2: intros ??; cbn; eauto. eapply main_lemma with (u := 0) (v := 1) in T1 as (I & S & H); trivial. 2, 3: intros (?&?&?) % vars_ren; discriminate. exists I. intuition idtac. revert EQ. cbn -[enc]. rewrite !enc_subst_id; trivial. rewrite !AppR_subst; rewrite ?Enc_subst_id; trivial; cbn -[add]. all: unfold funcomp; cbn -[add]; rewrite !ren_plus_base, !ren_plus_combine; change (1 + 1) with 2. specialize (H (heads C)) as H1; mp H1; simplify; trivial. specialize (H (tails C)) as H2; mp H2; simplify; trivial. destruct H1 as [t' [-> H1]], H2 as [t'' [-> H2]]. rewrite <-!select_map, !enc_concat, <-!enc_app. intros EQ % equiv_lam_elim % equiv_lam_elim. eapply enc_eq in EQ. 1 - 2: intuition idtac. lia. all: intros s; try eapply H1; try eapply H2. 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)