proposition: Lemma subset_union_2 : forall E1 E2 F1 F2, E1 \c F1 -> E2 \c F2 -> (E1 \u E2) \c (F1 \u F2).
proof: Proof. Proof using. introv H1 H2. intros x. do 2 rewrite* in_union. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)