proposition: Lemma in_union : forall x E F, x \in (E \u F) = ((x \in E) \/ (x \in F)).
proof: Proof. Proof using. unfold mem, union. simpl. intros. rewrite in_union_eq. autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)