proposition: Lemma identity_composition_left (M : Metacategory) : ∀ f g fg u, identity M u -> composite M f g fg -> defined u f (pairs M) -> defined u fg (pairs M).
proof: Proof. intros. destruct H as [_ c0]. apply composite_defined with (h:=fg); auto; try solve [ apply c0 ]. Qed.
imports: Coq.Structures.DecidableTypeEx Coq.FSets.FMapFacts Category.Lib.FMapExt Coq.Arith.PeanoNat Category.Lib Category.Theory.Category