proposition: Lemma ordertyping_termination_steps Gamma n s A: Gamma ⊢(n) s : A -> exists t, s ▷ t.
proof: Proof. now intros ? % ordertyping_soundness % termination_steps. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)