{Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {motive : SlashInvariantForm Γ k → Sort u} →
      ((toFun : UpperHalfPlane → ℂ) →
          (slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun) →
            motive { toFun := toFun, slash_action_eq' := slash_action_eq' }) →
        (t : SlashInvariantForm Γ k) → motive t