proposition: Lemma add_transpose_neqkey elt : transpose_neqkey (@Equal elt) (@add elt ) .
proof: Proof. unfold transpose_neqkey; intros. eapply Equal_mapsto_iff; split; intros. - rewrite add_mapsto_iff in *; intuition; subst. destruct (E.eq_dec k0 k'); intuition; eauto. rewrite e in H0; intuition. rewrite add_mapsto_iff in H2; intuition. - rewrite add_mapsto_iff in *; intuition; subst. destruct (E.eq_dec k0 k); intuition; eauto. rewrite e1 in H0; intuition. rewrite add_mapsto_iff in H2; 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