proposition: Lemma orderlisttyping_preservation_under_substitution Gamma n S L Delta sigma: Gamma ⊢₊(n) S : L -> Delta ⊩(n) sigma : Gamma -> Delta ⊢₊(n) sigma •₊ S : L.
proof: Proof. induction 1; cbn; (eauto 4). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)