proposition: Lemma tensor_id_right_inj {x y} (f g : x ~> y) : f ⨂ id[I] ≈ g ⨂ id[I] → f ≈ g.
proof: Proof. intros. rewrite <- id_right; symmetry; rewrite <- id_right; symmetry. rewrite <- (iso_to_from unit_right). rewrite !comp_assoc. rewrite !to_unit_right_natural. rewrites; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal