proposition: Lemma closure_under_reduction s t A: s >* t -> E A t -> E A s.
proof: Proof. intros H [v [[H1 H2] H3]]. exists v; intuition. split; eauto. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)