proposition: Lemma termination_steps Gamma s A: Gamma ⊢ s : A -> exists t, s ▷ t.
proof: Proof. intros H % semantic_soundness. specialize (H var (@G_id X Gamma)). asimpl in H; unfold id in H. eapply E_evaluates, H. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)