∀ (M : Type u_1) (N : Type u_2) (P : Type u_3) [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P],
  (AddMonoid.Coprod.lift (AddMonoid.Coprod.map (AddMonoidHom.id M) AddMonoid.Coprod.inl)
          (AddMonoid.Coprod.inr.comp AddMonoid.Coprod.inr)).comp
      (AddMonoid.Coprod.lift (AddMonoid.Coprod.inl.comp AddMonoid.Coprod.inl)
        (AddMonoid.Coprod.map AddMonoid.Coprod.inr (AddMonoidHom.id P))) =
    AddMonoidHom.id (AddMonoid.Coprod M (AddMonoid.Coprod N P))