proposition: Lemma varof_ren f x (s: exp X): varof x (ren f s) -> exists y, x = f y /\ varof y s.
proof: Proof. induction s in x, f |-*; cbn; intuition. - exists f0; intuition. now inv H. - inv H. - inv H. eapply IHs in H1 as []. intuition. destruct x0; try discriminate. exists x0. intuition. - inv H; [edestruct IHs1 | edestruct IHs2]; eauto; eexists; intuition; eauto. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)