{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {S : Subgroup G} →
        [DecidableRel ⇑(QuotientGroup.rightRel S)] →
          (A : Rep k ↥S) → [S.FiniteIndex] → Rep.ind S.subtype A ≅ Rep.coind S.subtype A