{Props : Type} →
  {motive : ProofWidgets.Component Props → Sort u} →
    ((toModule : Lean.Widget.Module) → («export» : String) → motive { toModule := toModule, «export» := «export» }) →
      (t : ProofWidgets.Component Props) → motive t