proposition: Theorem eq_set_empty : forall {A} (l1 l2: list A), eq_set l1 l2 -> l1 = [] -> l2 = [].
proof: Proof. introv Heqs Heql. apply null_iff_nil. introv v. apply eq_set_iff_eq_set2 in Heqs. apply Heqs in v. subst. inverts v. Qed.
imports: UsefulTypes bin_rels Omega