{α : Type} →
  {motive : Lean.Doc.FromDocArg α → Sort u} →
    ((fromDocArg : Lean.Doc.DocArg → Lean.Elab.TermElabM α) → motive { fromDocArg := fromDocArg }) →
      (t : Lean.Doc.FromDocArg α) → motive t