proposition: Lemma add_Equal_simple : forall {TValue} {m1 m2: t TValue}, Equal m1 m2 -> forall k v, Equal (add k v m1) (add k v m2).
proof: Proof. intros. apply add_m; eauto. 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