law eq_of_is_eq

bend-mathlib@0.8.1.0 · nat.bend:1296

import Base

1296# If the equality test says true, the naturals are equal.
1297law eq_of_is_eq:
1298  for a: Nat
1299  for b: Nat
1300  for h: {Nat.is_eq(a, b) == True{} : Bool}
1301  {a == b : Nat}