proposition: Lemma lKeepDisjoint : forall {T : Type} (deq : Deq T) (ll keep: list T), disjoint keep ll -> lKeep deq keep ll = [].
proof: Proof. induction ll; cpx. introv Hdis. repeat (disjoint_reasoning). simpl. rw memberb_din. cases_if; sp. contradiction. Qed.
imports: UsefulTypes bin_rels Omega