proposition: Lemma map_add {A B}: forall (f : A -> B) m k v, Equal (map f (add k v m)) (add k (f v) (map f m)).
proof: Proof. unfold Equal; intros; case_eq (find y (add k (f v) (map f m))); case_eq (find y (map f (add k v m))); intros; eauto. - rewrite <- find_mapsto_iff in H, H0. rewrite map_mapsto_iff in H; destruct H as [a [b_eq In_b]]; subst. rewrite add_mapsto_iff in H0, In_b; intuition; subst; eauto. rewrite map_mapsto_iff in H3; destruct H3 as [a' [b_eq' In_b']]; subst. rewrite find_mapsto_iff in In_b', H2; congruence. - rewrite <- find_mapsto_iff in H0. rewrite <- not_find_in_iff in H; exfalso; apply H. rewrite add_mapsto_iff in H0; intuition; subst; eauto. rewrite H0, map_in_iff, add_in_iff; eauto. rewrite map_mapsto_iff in H2; destruct H2 as [a [b_eq In_b]]; subst. rewrite map_in_iff, add_in_iff; right; econstructor; eauto. - rewrite <- find_mapsto_iff in H. rewrite <- not_find_in_iff in H0; exfalso; apply H0. rewrite map_mapsto_iff in H; destruct H as [a [b_eq In_b]]; subst. rewrite add_mapsto_iff in In_b; intuition; subst; eauto. rewrite H1, add_in_iff; eauto. rewrite add_in_iff, map_in_iff; right; econstructor; 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