proposition: Lemma tab_typing {X} n (f: nat -> exp X) g k Gamma: (forall i, Gamma ⊢(n) f i : g i) -> Gamma ⊢₊(n) tab f k : tab g k.
proof: Proof. intros; induction k; cbn; (eauto 2). eapply orderlisttyping_app; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)