{m : Type → Type} →
  {motive : Lean.Elab.MonadParentDecl m → Sort u} →
    (t : Lean.Elab.MonadParentDecl m) →
      ((getParentDeclName? : m (Option Lean.Name)) → motive { getParentDeclName? := getParentDeclName? }) → motive t