proposition: Lemma multiple_adds : forall {TValue} k v1 v2 (m: t TValue), Equal (add k v2 (add k v1 m)) (add k v2 m).
proof: Proof. intros. unfold Equal. intros k'. destruct (E.eq_dec k k'). rewrite !add_eq_o; eauto. rewrite !add_neq_o; 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