proposition: Lemma ALEndoMapFilterCommute : forall {KA VA VB : Type} (DKA : Deq KA) (fk : KA -> KA) (fv : VA -> VB), injective_fun fk -> forall (sub : AssocList KA VA) l, (ALFilter DKA (ALMap fk fv sub) (map fk l)) = ALMap fk fv (ALFilter DKA sub l).
proof: Proof. intros. apply ALMapFilterCommute; auto. Qed.
imports: list Omega