proposition: Lemma map_var_typing n Gamma N L: N ⊆ dom Gamma -> select N Gamma = L -> ord' L <= n -> Gamma ⊢₊(n) map var N : L.
proof: Proof. induction N in L |-*; cbn; intuition. - destruct L; try discriminate; intuition. - specialize (H a) as H'; mp H'; (intuition (auto with datatypes)); domin H'. rewrite H' in H0. subst. econstructor. all: cbn in H1; simplify in H1; intuition. eapply IHN; (eauto 1); lauto. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)