proposition: Lemma ALFindFilterSome : forall l v t sub, (ALFind (ALFilter sub l) v = Some t) <=> (ALFind sub v = Some t # ! LIn v l).
proof: Proof. induction sub; simpl; sp; split; introv H; sp; allsimpl. - destruct (in_deq Key DeqKey a0 l); allsimpl. + rw IHsub in H; sp;case_if as Hd; subst;auto; try contradiction. + case_if as Hd; subst; auto; try contradiction. rw IHsub in H; exrepnd; auto. - destruct (in_deq Key DeqKey a0 l); allsimpl. + apply IHsub in H; exrepnd; auto. + destruct (DeqKey v a0); allsimpl; subst; sp;[]. rw IHsub in H; exrepnd; auto. - destruct (in_deq Key DeqKey a0 l); allsimpl. + apply IHsub; split; auto. destruct (DeqKey v a0); allsimpl; subst; sp. + destruct (DeqKey v a0); allsimpl; subst; sp. apply IHsub; split; auto. Qed.
imports: list Omega