law length_reverse_sym

bend-mathlib@0.8.1.0 · string.bend:625

import Base

625# Reversing preserves the length, reversed to rewrite toward the simple side.
626law length_reverse_sym:
627  for s: String
628  {String.length(s) == String.length(String.reverse(s)) : Nat}