proposition: Lemma filter_false_eq_empty : forall m, Equal (filter (fun (_ : key) (_ : list nat) => false) m) (empty _).
proof: Proof. unfold filter; simpl. intros; rewrite fold_1; induction (elements m); simpl; eauto. reflexivity. 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