proposition: Lemma lKeepSubset : forall {T : Type} (deq : Deq T) (ll keep: list T), subset (lKeep deq keep ll) ll.
proof: Proof. induction ll; cpx. introv Hdis. repeat (disjoint_reasoning). allsimpl. rw memberb_din in Hdis. cases_if; allsimpl; try dorn Hdis; cpx; apply IHll in Hdis; cpx. Qed.
imports: UsefulTypes bin_rels Omega