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