1	import Base
2	import ../../../src/containers/balanced_search_tree.bend as M
3	import ../../../src/containers/types/dynamic_array.bend as DE
4	
5	# Universal local laws for the traversal optimization, not a proof of the
6	# complete indexed TreeMap or of arbitrary iterator histories.
7	def choice_equivalent(+x: Nat, +p: Nat, +q: Nat, +found: Bool) -> {M.ascend_choice(x, p, q, found) == M.pick(M.Ascend, found, M.Ascend{0n, p, True{}}, M.Ascend{x, q, False{}}) : M.Ascend}:
8	  match found:
9	    case False{}:
10	      {==}
11	    case True{}:
12	      {==}