proposition: Lemma ALMapFilterCommute : forall {KA KB VA VB : Type} (DKA : Deq KA) (DKB : Deq KB) (fk : KA -> KB) (fv : VA -> VB), injective_fun fk -> forall (sub : AssocList KA VA) l, (ALFilter DKB (ALMap fk fv sub) (map fk l)) = ALMap fk fv (ALFilter DKA sub l).
proof: Proof. introv Hin. induction sub; simpl; sp; allsimpl. cases_ifd Hd; cases_ifd Hc; simpl; auto; f_equal; auto. - apply in_map_iff in Hdt. exrepnd. apply Hin in Hdt0. subst. cpx. - rw in_map_iff in Hdf. provefalse. apply Hdf. eexists; eauto. Qed.
imports: list Omega