proposition: Lemma union_empty a b : union a b [=] empty <-> a [=] empty /\ b [=] empty.
proof: Proof. rewrite !empty_subset. split; intro h. split; trans (union a b). apply union_subset_1. hyp. apply union_subset_2. hyp. apply union_subset_3; tauto. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)