proposition: Theorem monoidal_naturality : natural (@unit_left _ M) * natural (@unit_right _ M) * natural (@tensor_assoc _ M).
proof: Proof. prove_naturality M normal. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal