String.to_list_from_list_sym: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/string.bend as String
Lines 700-703 of bend-mathlib@0.8.1.0/string.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/string.bend&start_line=700&end_line=703

import Base

# Converting a character list to a string and back gives the list, reversed to rewrite toward the simple side.
law to_list_from_list_sym:
  for cs: List<&2, Char>
  {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.from_list
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=to_list_from_list