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