{α : Sort u_1} →
  {motive : Lean.Doc.Ref✝ α → Sort u} →
    (t : Lean.Doc.Ref✝¹ α) →
      ((content : α) →
          (location : Lean.Syntax) →
            (seen : Bool) → motive { content := content, location := location, seen := seen }) →
        motive t