{motive : ProofWidgets.RpcEncodablePacket✝ → Sort u} →
  ((pos goals : Lean.Json) →
      (termGoal? : Option Lean.Json) →
        (selectedLocations : Lean.Json) →
          motive { pos := pos, goals := goals, termGoal? := termGoal?, selectedLocations := selectedLocations }) →
    (t : ProofWidgets.RpcEncodablePacket✝) → motive t