proposition: Lemma ALFindFilterNone : forall l v sub, (ALFind (ALFilter sub l) v = None) <=> (ALFind sub v = None [+] LIn v l).
proof: Proof. induction sub; simpl; sp; split; introv H; sp; allsimpl. - destruct (in_deq Key DeqKey a0 l); allsimpl; destruct (DeqKey v a0) as [ddd | ddd]; allsimpl; subst; try(rw IHsub in H); exrepnd; auto;cpx. - destruct (in_deq Key DeqKey a0 l); allsimpl; destruct (DeqKey v a0) as [ddd | ddd]; allsimpl; subst;cpx;apply IHsub; cpx. - destruct (in_deq Key DeqKey a0 l); allsimpl; destruct (DeqKey v a0) as [ddd | ddd]; allsimpl; subst;cpx;apply IHsub; cpx. Qed.
imports: list Omega