law cmp_refl_sym

bend-mathlib@0.8.1.0 · bool.bend:777

import Base

777# Comparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.
778law cmp_refl_sym:
779  for b: Bool
780  {EQ{} == Bool.cmp(b, b) : Cmp}