[STATEMENT]
lemma (in is_functor) op_cf_obj_comma_ArrMap_vdomain[cat_comma_cs_simps]:
  "\<D>\<^sub>\<circ> (op_cf_obj_comma \<FF> b\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_cf_obj_comma \<FF> b\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding op_cf_obj_comma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_cf_comma \<FF> (dghm_const (cat_1 []\<^sub>\<circ> []\<^sub>\<circ>) \<BB> b (\<BB>\<lparr>CId\<rparr>\<lparr>b\<rparr>))\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>
[PROOF STEP]
by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_comma_cs_simps cat_cf_obj_comma_def[symmetric]
    )