{Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {motive : CuspForm Γ k → Sort u} →
      ((toSlashInvariantForm : SlashInvariantForm Γ k) →
          (holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑toSlashInvariantForm) →
            (zero_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k) →
              motive
                { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := zero_at_cusps' }) →
        (t : CuspForm Γ k) → motive t