{motive : Lean.CollectFVars.State → Sort u} →
  (t : Lean.CollectFVars.State) →
    ((visitedExpr : Lean.ExprSet) →
        (fvarSet : Lean.FVarIdSet) →
          (fvarIds : Array Lean.FVarId) →
            motive { visitedExpr := visitedExpr, fvarSet := fvarSet, fvarIds := fvarIds }) →
      motive t