proposition: Lemma E_var x A: E A (var x).
proof: Proof. exists (var x). unfold evaluates; cbn; intuition. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)