NativeMap.string_comparison_original_identity: law of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as NativeMap
Lines 335-338 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&start_line=335&end_line=338

import Base

law string_comparison_original_identity:
  for +a: String
  for +b: String
  comparison_identity(String, a, b, comparison_tag(String, String.cmp(a, b)))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&name=comparison_identity
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&name=comparison_result_identity
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&name=comparison_tag
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&name=string_comparison_identity
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend&name=string_comparison_shape