proposition: Lemma in_union_extract_1 : forall x l1, x \in (\{x} \u l1).
proof: Proof. Proof using. intros. apply in_union_get_1. apply in_single_self. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)