proposition: Lemma ren_closed_E A: ren_closed (E A).
proof: Proof. eapply ren_closed_C, ren_closed_V. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)