law eq_of_cmp_eq

bend-mathlib@0.8.1.0 · bool.bend:423

import Base

423# Two booleans that compare EQ are equal.
424law eq_of_cmp_eq:
425  for a: Bool
426  for b: Bool
427  for h: {Cmp.is_eq(Bool.cmp(a, b)) == True{} : Bool}
428  {a == b : Bool}