proposition: Lemma vars_varof x s: x ∈ vars s -> varof x s.
proof: Proof. induction s in x |-*; cbn; intuition. - subst; eauto. - econstructor. eapply IHs. mapinj. destruct x0. + eapply remove_In in H1; intuition. + cbn. now eapply remove_prev in H1. - simplify in H; intuition. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)