{motive : ProofWidgets.ExprPresentationProps → Sort u} →
  (t : ProofWidgets.ExprPresentationProps) →
    ((expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx) → motive { expr := expr }) → motive t