proposition: Lemma mapsto_inv : ∀ elt f g (fg : elt) x y z m, M.MapsTo (f, g) fg (M.add (x, y) z m) -> (x = f ∧ y = g ∧ z = fg) ∨ M.MapsTo (f, g) fg m.
proof: Proof. intros. apply add_mapsto_iffT in H. destruct H; simpl in *; intuition. Defined.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor