∀ {mvarsToCheckType mvarsToCheckType_1 : Array Lean.MVarId},
  Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType =
      Lean.Meta.Sym.MkPreResultResult.success✝¹ mvarsToCheckType_1 →
    mvarsToCheckType = mvarsToCheckType_1