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