proposition: Lemma ren_varof x f (s: exp X): varof x s -> varof (f x) (ren f s).
proof: Proof. enough (varof x s -> forall y, y = f x -> varof y (ren f s)) by eauto. induction 1 in f |-*; cbn; eauto. - intros ? ->; eauto. - intros ? ->; econstructor; now eapply IHvarof. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)