proposition: Lemma eqsetSubset : forall {T : Type} (la lb : list T), (subset la lb # subset lb la) <=> eqset la lb.
proof: Proof. intros; unfold eqset; unfold subset; split; introns Hyp; repnd; dands; intros; cpx; apply Hyp; cpx. Qed.
imports: UsefulTypes bin_rels Omega