proposition: Lemma ginst_typing I: [alpha] ⊢(3) ginst I : (alpha → alpha) → alpha.
proof: Proof. econstructor. eapply AppL_ordertyping_repeated. eapply repeated_ordertyping. intros ? ? % repeated_in; subst; [auto|..]. reflexivity. econstructor; (eauto 2). 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)