∀ (ref m returnType : Lean.Syntax) (mutableVars : Lean.Elab.Term.Do.VarSet) (insideFor : Bool),
  sizeOf { ref := ref, m := m, returnType := returnType, mutableVars := mutableVars, insideFor := insideFor } =
    1 + sizeOf ref + sizeOf m + sizeOf returnType + sizeOf mutableVars + sizeOf insideFor