law seek_high_shape

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_insert.bend:364

import Base

364law seek_high_shape:
365  for -V: Data
366  for p: Nat
367  for lo: Map<&2, V>
368  for hi: Map<&2, V>
369  for key: String
370  for r: Map<&2, V> & String & Maybe<&2, String>
371  for e: {r == (hi, key, seek_found(V, r)) : Map<&2, V> & String & Maybe<&2, String>}
372  {Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r) == (MNode{p, lo, hi}, key, seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r))) : Map<&2, V> & String & Maybe<&2, String>}