proposition: Lemma Lambda_typing Gamma L B k s: length L = k -> rev L ++ Gamma ⊢ s : B -> Gamma ⊢ (Lambda k s) : Arr L B.
proof: Proof. induction k in L, Gamma, s |-*. - destruct L; try discriminate. intros _; cbn; (eauto 2). - destruct L; try discriminate. intros H; injection H as H. cbn; intros; econstructor. eapply IHk; (eauto 2). now rewrite <-app_assoc in H0. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)