proposition: Lemma map_empty : forall elt elt' f, Equal (map f (empty elt)) (empty elt').
proof: Proof. intros; eapply Equal_mapsto_iff; split; intros. - destruct (map_2 (elt' := elt') (m := empty elt) (x := k) (f := f)). + eexists; eauto. + apply empty_1 in H0; intuition. - apply empty_1 in H; intuition. 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