law eq_of_eq_true

bend-mathlib@0.8.1.0 · string.bend:336

import Base

336# Two strings that String.eq calls equal are equal.
337law eq_of_eq_true:
338  for a: String
339  for b: String
340  for h: {String.eq(a, b) == True{} : Bool}
341  {a == b : String}