proposition: Lemma ALMapRangeFilterCommute : forall K V l T (deq : Deq K) (f: V -> T) (sub : AssocList K V), (ALFilter deq (ALMapRange f sub) l) = ALMapRange f (ALFilter deq sub l).
proof: Proof. induction sub; simpl; sp; allsimpl. cases_if; simpl; auto; f_equal; auto. Qed.
imports: list Omega