+ refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
+ ; car_one := iso_id [] |}
+ ; intros; unfold hom; simpl
+ ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancell; auto.
+
+ apply ndr_structural_indistinguishable; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_comp; auto.
+ apply nd_structural_copy; auto.
+ apply nd_structural_prod; auto.
+ apply nd_structural_comp; auto.
+ apply weak'_structural.
+ apply nd_structural_id0; auto.
+ apply nd_structural_cancelr; auto.