proposition: Lemma E_evaluates s A: E A s -> exists t, s ▷ t.
proof: Proof. intros (t & H1 & H2); exists t; intuition. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)