proposition: Lemma ALDomFilterCommute : forall l sub, diff DeqKey l (ALDom sub) = ALDom (ALFilter sub l).
proof: Proof. induction sub; simpl; sp; allsimpl. - apply diff_nil. - rewrite diff_cons_r. rw memberb_din. cases_if; simpl; f_equal; auto. Qed.
imports: list Omega