Lemma cancell_coherent (b:enr_v K) :
#(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
(#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
Lemma cancell_coherent (b:enr_v K) :
#(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
(#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>