proposition: Lemma varof_vars x s: varof x s -> x ∈ vars s.
proof: Proof. induction 1; cbn; eauto. 1 - 2: eapply in_app_iff; intuition. eapply in_map_iff. exists (S x). intuition. eapply remove_remain; eauto. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)