proposition: Lemma ALRangeRelFilter : forall R (subl subr : AssocList) l, ALRangeRel R subl subr -> ALRangeRel R (ALFilter subl l) (ALFilter subr l).
proof: Proof. induction subl as [| (kl,vl) subl Hind]; introv Hal; destruct subr as [| (kr,vr) subr]; allsimpl; repnd; dands; subst; cpx. cases_if; cpx. Qed.
imports: list Omega