∀ {F : Type u_1 → Type u_2}
  (motive :
    (x x_1 : Functor F) →
      LawfulFunctor F → LawfulFunctor F → (∀ (α β : Type u_1) (f : α → β) (x_4 : F α), f <$> x_4 = f <$> x_4) → Prop)
  (x x_1 : Functor F) (x_2 : LawfulFunctor F) (x_3 : LawfulFunctor F)
  (x_4 : ∀ (α β : Type u_1) (f : α → β) (x_4 : F α), f <$> x_4 = f <$> x_4),
  (∀ (m : {α β : Type u_1} → (α → β) → F α → F β) (mc : {α β : Type u_1} → α → F β → F α)
      (m' : {α β : Type u_1} → (α → β) → F α → F β) (mc' : {α β : Type u_1} → α → F β → F α) (H1 : LawfulFunctor F)
      (H2 : LawfulFunctor F) (H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x),
      motive { map := m, mapConst := mc } { map := m', mapConst := mc' } H1 H2 H) →
    motive x x_1 x_2 x_3 x_4