proposition: Lemma ren_closed_V A: ren_closed (V A).
proof: Proof. induction A as [beta | A IHA B IHB]. - intros ? ? []. - intros delta []; cbn in *; eauto; intros [H1 H2]. split; eauto using normal_ren. intros t delta' H'. asimpl. replace (_ • e) with (ren (upRen_exp_exp (delta >> delta')) e)by now asimpl. now eapply H2. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)