; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f