proposition: Lemma assert_eqsetb : forall T eq, forall l1 l2 : list T, assert (eqsetb eq l1 l2) <=> forall x, LIn x l1 <=> LIn x l2.
proof: Proof. sp; unfold eqsetb; trw assert_of_andb; repeat (trw assert_subsetb); repeat (split; sp); apply_in_hyp p; auto. Qed.
imports: UsefulTypes bin_rels Omega