proposition: Lemma add_associative {elt} (k : M.key) (e : elt) (k0 : M.key) (e0 : elt) (z : M.t elt) : (E.eq k k0 → e = e0) → M.Equal (M.add k e (M.add k0 e0 z)) (M.add k0 e0 (M.add k e z)).
proof: Proof. intros H addr. rewrite !F.add_o. destruct (E.eq_dec k addr); destruct (E.eq_dec k0 addr); eauto. apply E.eq_sym in e2. pose proof (E.eq_trans e1 e2). rewrite (H H0). reflexivity. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts