{motive : Lean.Widget.InfoPopup → Sort u} →
  (t : Lean.Widget.InfoPopup) →
    ((type exprExplicit : Option Lean.Widget.CodeWithInfos) →
        (doc : Option String) → motive { type := type, exprExplicit := exprExplicit, doc := doc }) →
      motive t