proposition: Lemma assert_subsetb : forall T eq, forall l1 l2 : list T, assert (subsetb eq l1 l2) <=> forall x, LIn x l1 -> LIn x l2.
proof: Proof. sp; unfold subsetb. trw assert_nullb; trw null_diff; split; sp. Qed.
imports: UsefulTypes bin_rels Omega