∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w))
  (map_id : ∀ (v : V), map (CategoryTheory.ReflQuiver.id v) = CategoryTheory.CategoryStruct.id (obj v)) (v : V),
  (CategoryTheory.Cat.FreeRefl.lift' obj (fun {v w} => map) map_id).obj (CategoryTheory.Cat.FreeRefl.mk v) = obj v