proposition: Lemma Vars__de_in e E: e ∈ E -> forall y, y ∈ vars__de e -> y ∈ Vars__de E.
proof: Proof. unfold Vars__de; intros; eapply nodup_In, in_flat_map. exists e. intuition. Qed.
imports: Arith Lia List Undecidability.HOU(std.std calculus.prelim)