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