(motive : MProd Lean.FVarIdSet (MProd (Array Lean.FVarId) Bool) → Sort u_1) →
  (r : MProd Lean.FVarIdSet (MProd (Array Lean.FVarId) Bool)) →
    ((fvarIdSet : Lean.FVarIdSet) →
        (fvarIds : Array Lean.FVarId) → (modified : Bool) → motive ⟨fvarIdSet, fvarIds, modified⟩) →
      motive r