proposition: Lemma ALKeepFirstFilterDiff: forall sub lvk lvf, (ALKeepFirst sub (diff DeqKey lvf lvk)) = (ALKeepFirst (ALFilter sub lvf) lvk).
proof: Proof. induction sub; allsimpl; autorewrite with fast; cpx;[]. intros. allsimpl. destruct a. cases_ifd H1d; cases_ifd H2d; allrw in_diff; exrepnd; allsimpl; cpx. - cases_ifd H3d; cpx. f_equal. rw <- diff_remove. apply IHsub. - cases_ifd H3d; cpx. provefalse. apply H1df. dands;cpx. Qed.
imports: list Omega