law char_cmp_refl_sym

bend-mathlib@0.8.1.0 · string.bend:601

import Base

601# Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
602law char_cmp_refl_sym:
603  for c: Char
604  {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}