{motive : Lean.Widget.ExprDiffTag✝ → Sort u} →
  motive Lean.Widget.ExprDiffTag.change✝ →
    motive Lean.Widget.ExprDiffTag.delete✝ →
      motive Lean.Widget.ExprDiffTag.insert✝ → (t : Lean.Widget.ExprDiffTag✝¹) → motive t