fact: Fixpoint ALFilter (sub : AssocList) (keys : list Key) : AssocList := match sub with | nil => nil | (k, v) :: xs => if (in_deq _ DeqKey k keys) then ALFilter xs keys else (k, v) :: ALFilter xs keys end.
imports: list Omega