proposition: Lemma finst_typing I n : I ⊆ nats n -> [alpha] ⊢(3) finst I n : Arr (repeat (alpha → alpha) n) alpha.
proof: Proof. intros H; eapply Lambda_ordertyping; simplify; (eauto 1). eapply AppL_ordertyping_repeated. eapply repeated_ordertyping; simplify; (eauto 1). intros; mapinj. econstructor; simplify; cbn; [auto|]. rewrite nth_error_app1; simplify; (eauto 1). eapply nth_error_repeated; (eauto 1). 1 - 2: eapply nats_lt, H, H2. econstructor; simplify; (auto 2). rewrite nth_error_app2; simplify; (eauto 1). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)