proposition: Lemma PCP_MU S: PCP S -> OU 3 X (PCP_to_U S).
proof: Proof. intros (I & ? & ? & ?). pose (sigma := finst I (length S) .: ginst I .: var). exists [alpha]. exists sigma. split. - intros x A. destruct x as [| [| x]]; try discriminate; cbn. 3: intros [] % nth_error_In. all: injection 1 as ?; subst. eapply finst_typing; (auto 2). eapply ginst_typing. - cbn -[ginst]. do 3 eapply equiv_lam_proper. eapply equiv_app_proper. eapply equiv_app_proper. reflexivity. all: unfold shift, var_zero. all: rewrite !AppR_subst; rewrite ?Enc_subst_id; (auto 2). 2: rewrite map_id_list. 3: intros ? ? % repeated_in; subst; reflexivity. all: cbn; rewrite !ren_plus_base, !ren_plus_combine; change (1 + 1 + 1) with 3. 2: rewrite !AppL_ren; simplify; cbn [ren]; unfold upRen_exp_exp. 2: unfold up_ren, funcomp; cbn [scons]. replace (|S|) with (|heads S|) at 1 by now simplify. replace (|S|) with (|tails S|) at 1 by now simplify. rewrite !finst_equivalence, H1; simplify; (auto 2). rewrite ginst_equivalence; trivial. unfold ginst; asimpl. now simplify. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)