∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep k G} {B : Rep k H}
  {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : A ⟶ (Action.res (ModuleCat k) f₁).obj B} {T : Type u_1}
  (F : (f : G →* H) → (A ⟶ (Action.res (ModuleCat k) f).obj B) → T), F f₁ φ = F f₂ (h ▸ φ)