proposition: Lemma orderlisttyping_element Gamma n S L: Gamma ⊢₊(n) S : L -> forall s, s ∈ S -> exists A, Gamma ⊢(n) s : A /\ A ∈ L.
proof: Proof. induction 1; cbn; intros; intuition; subst. eexists; intuition; (eauto 2). edestruct IHorderlisttyping; (eauto 1); intuition; eexists; split; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)