{motive : Lean.Meta.Rewrites.SideConditions → Sort u} →
  (t : Lean.Meta.Rewrites.SideConditions) →
    motive Lean.Meta.Rewrites.SideConditions.none →
      motive Lean.Meta.Rewrites.SideConditions.assumption →
        motive Lean.Meta.Rewrites.SideConditions.solveByElim → motive t