proposition: Lemma in_union_get_1 : forall x l1 l2, x \in l1 -> x \in (l1 \u l2).
proof: Proof. Proof using. intros. apply in_union_l. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)