{motive : Lean.Elab.Tactic.Do.SpecAttr.SpecProof → Sort u} →
  (t : Lean.Elab.Tactic.Do.SpecAttr.SpecProof) →
    t.ctorIdx = 0 →
      ((declName : Lean.Name) → motive (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global declName)) → motive t