String.eq_of_eq_true: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/string.bend as String
Lines 336-341 of bend-mathlib@0.8.1.0/string.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/string.bend&start_line=336&end_line=341

import Base

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

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.cmp
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_cmp_true_eq
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_eq_true_cmp
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_false_ne_true
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_step