MapLookup.accumulator_included: law of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend as MapLookup
Lines 143-150 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend&start_line=143&end_line=150

import Base

law accumulator_included:
  for -V: Data
  for tree: Map<&2, Maybe<&2, V>>
  for +acc: List<&2, Sigma<&2, &2, String, _ => Maybe<&2, V>>>
  for +key: String
  for +value: V
  for member: listed(V, acc, key, value)
  listed(V, Map.to_list.go(&2, Maybe<&2, V>, tree, acc), key, value)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map.to_list.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend&name=listed