law cmp_refl_sym

bend-mathlib@0.8.1.0 · string.bend:609

import Base

609# Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
610law cmp_refl_sym:
611  for s: String
612  {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}