law char_eq_of_is_eq

bend-mathlib@0.8.1.0 · string.bend:303

import Base

303# Two characters that Char.is_eq calls equal are equal.
304law char_eq_of_is_eq:
305  for a: Char
306  for b: Char
307  for h: {Char.is_eq(a, b) == True{} : Bool}
308  {a == b : Char}