proposition: Lemma redtm_typing w W: redctx (length W) ⊢(3) redtm w W : (alpha → alpha) → (alpha → alpha) → alpha.
proof: Proof. unfold redctx; do 3 econstructor. - eapply enc_typing; eauto. - eapply AppR_ordertyping;[ eapply Enc_typing|]; simplify; econstructor; cbn; simplify; eauto. 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)