proposition: Lemma eqs_typing_preservation_subst Gamma E L Delta sigma: Gamma ⊢₊₊ E : L -> Delta ⊩ sigma : Gamma -> Delta ⊢₊₊ sigma •₊₊ E : L.
proof: Proof. induction 1; cbn; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)