{motive : Lean.Meta.CaseValuesSubgoal → Sort u} →
  (t : Lean.Meta.CaseValuesSubgoal) →
    ((mvarId : Lean.MVarId) →
        (newHs : Array Lean.FVarId) →
          (subst : Lean.Meta.FVarSubst) → motive { mvarId := mvarId, newHs := newHs, subst := subst }) →
      motive t