proposition: Lemma filter_list_filter_fmap : forall {A: Type} m pred, SetEq (List.filter pred (GetValues (A:=A) m)) (GetValues (filter (ValueFilter pred) m)).
proof: Proof. intros. unfold SetEq; intuition. unfold GetValues. rewrite filter_In in H. destruct H as [inL sat]. unfold GetValues in inL. apply in_map_iff in inL. destruct inL as [x0 (ok, inL)]. destruct x0. apply in_elements_mapsto in inL. subst. simpl. apply (InA_In_snd k). apply elements_mapsto_iff. rewrite filter_iff. intuition. eauto using ValueFilter_proper. unfold GetValues in *. rewrite filter_In. rewrite in_map_iff in H. destruct H as [(k, e) (is_snd, is_in)]. apply in_elements_mapsto in is_in. rewrite filter_iff in is_in; eauto using ValueFilter_proper. destruct is_in as [maps_to sat]. compute in sat. simpl in *. subst. intuition. rewrite elements_mapsto_iff in maps_to. apply (InA_In_snd k). trivial. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances