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