proposition: Lemma union_remove : forall E F G, (E \u F) \- G = (E \- G) \u (F \- G).
proof: Proof. Proof using. intros. apply fset_extens; intros x; repeat (first [ rewrite in_remove | rewrite in_union ]); autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)