proposition: Lemma ordertyping_preservation_under_steps n (s s': exp X) (Gamma: ctx) A: s >* s' -> Gamma ⊢(n) s : A -> Gamma ⊢(n) s' : A.
proof: Proof. induction 1 in Gamma, A |-*; eauto using ordertyping_preservation_under_reduction. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)