proposition: Lemma in_union_inv : forall x l1 l2, x \in (l1 \u l2) -> x \in l1 \/ x \in l2.
proof: Proof. Proof using. introv H. rewrite @in_union_eq in H. auto. typeclass. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)