(motive : MProd Lean.MVarId (Array Lean.FVarId) → Sort u_1) →
  (r : MProd Lean.MVarId (Array Lean.FVarId)) →
    ((mvarId : Lean.MVarId) → (newFVarIds : Array Lean.FVarId) → motive ⟨mvarId, newFVarIds⟩) → motive r