lean-0005: Substring comparison is not reflexive on malformed UTF-8

Substring == returned false when comparing a substring with itself if its positions were not valid UTF-8. Expr contains Substring transitively (through metadata and Syntax), and ExprMap is a HashMap, so non-reflexive equality on Substring undermines Expr-keyed maps. Found by the Lean4Lean verification.

Reproduction

Shows the bug on Lean v4.24.0. Adapted from #10511. bugs/lean-0005.lean

/-
On v4.24.0 this prints `false`. On v4.25.0 and later it prints `true`.
From the issue.
-/

#eval
  let s : Substring := ⟨"", ⟨1⟩, 0⟩
  s == s