A filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).