∀ {k G : Type u_1} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G} (A : Rep k ↥S)
  (f : ↑(Rep.coind S.subtype A).V) (g₁ g₂ : G),
  g₁ ≈ g₂ → (Representation.IndV.mk S.subtype A.ρ g₁) (↑f g₁) = (Representation.IndV.mk S.subtype A.ρ g₂) (↑f g₂)