proposition: Lemma ordertypingSubst_soundness n Delta (sigma: fin -> exp X) Gamma: Delta ⊩(n) sigma : Gamma -> Delta ⊩ sigma : Gamma.
proof: Proof. intros ????; eapply ordertyping_soundness; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)