import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/types/dynamic_array.bend as DE
import ./bk.bend as BK
import ./nsr.bend as NR
import ./nsf.bend as NF
import ./da.bend as DA
import ./state.bend as ST

# The TreeMap's node store (the ns_* functions of the implementation) on the
# realization of a node list xs of length at most 2^d, d <= l <= 31: a read
# returns the list's node, a write in range updates the list, an append
# snocs it (doubling the capacity when full and below the limit), clear
# empties it. These are the statements the dynamic-array lemmas of arr.bend
# make for a dynamic array of nodes.


def isj(-A: Data, m: Maybe<&2, A>) -> Bool:
  match m:
    case None{}:
      False{}
    case Some{x}:
      True{}

# a slot below the length holds something
def nth_isj(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {isj(A, SC.nth(A, xs, i)) == True{} : Bool}:
  match xs i:
    case Nil{} _:
      Empty.absurd({isj(A, SC.nth(A, Nil{}, i)) == True{} : Bool}, N.lt_zero_absurd(i, h))
    case Con{x, r} 0n:
      {==}
    case Con{x, +r} 1n+q:
      nth_isj(A, r, q, h)

def len_init(-A: Data, +xs: List<&2, A>, +m: Nat, +h: {SC.length(A, xs) == 1n+m : Nat}) -> {SC.length(A, SC.init(A, xs)) == m : Nat}:
  match xs m:
    case Nil{} _:
      Empty.absurd({SC.length(A, SC.init(A, Nil{})) == m : Nat}, N.zero_succ(m, h))
    case Con{x, Nil{}} 0n:
      {==}
    case Con{x, Nil{}} 1n+q:
      Empty.absurd({SC.length(A, SC.init(A, Con{x, Nil{}})) == 1n+q : Nat}, N.zero_succ(q, N.succ_inj(0n, 1n+q, h)))
    case Con{x, Con{y, t}} 0n:
      Empty.absurd({SC.length(A, SC.init(A, Con{x, Con{y, t}})) == 0n : Nat}, N.succ_zero(SC.length(A, t), N.succ_inj(1n+SC.length(A, t), 0n, h)))
    case Con{x, Con{+y, +t}} 1n+q:
      N.succ_cong(SC.length(A, SC.init(A, Con{y, t})), q, len_init(A, Con{y, t}, q, N.succ_inj(1n+SC.length(A, t), 1n+q, h)))

# a node is its encoding read back
def mk_enc(~K: Data, +y: M.Node<K>) -> {M.mk_node(~K, M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), M.nkey(~K, y)) == y : M.Node<K>}:
  match y:
    case M.Free{x}:
      {==}
    case M.N{True{}, lf, rt, pa, k}:
      {==}
    case M.N{False{}, lf, rt, pa, k}:
      {==}

# ---- length ----

def ns_length_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_length(~K, NR.real(~K, l, d, xs)) == (NR.real(~K, l, d, xs), SC.length(M.Node<K>, xs)) : M.NodeStore<K> & Nat}:
  {==}

# ---- read ----

def get_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
  %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, y)), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rt(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), M.nleft(~K, y)), NF.left_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rl(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), M.nright(~K, y)), NF.right_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rr(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), M.nleft(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.nparent(~K, y)), NF.parent_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rp(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  %Equal.sym(Array<Maybe<&2, K>> & Maybe<&2, K>, Array.get(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i)), (AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), M.nkey(~K, y)), NF.key_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rk(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  %Equal.sym(M.Node<K>, M.mk_node(~K, M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), M.nkey(~K, y)), y, mk_enc(~K, y)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))}, Done{_}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
  {==}

def gs(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, mv)) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, None{})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      get_some(~K, l, d, xs, hl, hd, hc, i, y, hmv)

def gc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, SC.nth(M.Node<K>, xs, i))) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
  match b:
    case True{}:
      gs(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), None{}, LL.nth_none(M.Node<K>, xs, i, N.not_lt_le(i, SC.length(M.Node<K>, xs), hb))) : {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, _)) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
      {==}

# a read returns the list's node (IndexOutOfRange past the length)
def ns_get_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_get(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, SC.nth(M.Node<K>, xs, i))) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
  gc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

# ---- write ----


def set_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, x)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{})), NF.key_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, x)), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{}))}, Done{Unit{}}) == (M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{}))}, Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  {==}

def ws(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y0}:
      set_some(~K, l, d, xs, hl, hd, hc, i, x, y0, hmv)

# a write below the length updates the list
def ns_set_in(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +h: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_set(~K, NR.real(~K, l, d, xs), i, x) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, _) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  ws(~K, l, d, xs, hl, hd, hc, i, x, SC.nth(M.Node<K>, xs, i), {==}, h)

# a write past the length changes nothing
def ns_set_out(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +h: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == False{} : Bool}) -> {M.ns_set(~K, NR.real(~K, l, d, xs), i, x) == (NR.real(~K, l, d, xs), Fail{DE.IndexOutOfRange{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), False{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, _) == (NR.real(~K, l, d, xs), Fail{DE.IndexOutOfRange{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  {==}

# ---- append ----


def push_at(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), x) == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}:
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.ntag(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.tag_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nleft(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nleft(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.left_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nright(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.right_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, x)), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.parent_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, x)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{})), NF.key_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
  %Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, xs, x)), 1n+SC.length(M.Node<K>, xs), LL.length_snoc(M.Node<K>, xs, x)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{}))} : M.NodeStore<K>}
  {==}

# with room: the node appended
def ns_push_room(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), True{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  Equal.cong(M.NodeStore<K>, M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, z => (z, Done{Unit{}}), M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), x), NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), push_at(~K, l, d, xs, hl, hd, hc, x, hn))

# full and below the limit: the blocks doubled, then the node appended
def ns_push_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == True{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  +hd1 = N.lt_succ_le_succ(d, l, hdl)
  +hc1 = N.le_trans(SC.length(M.Node<K>, xs), SC.pow2(d), SC.pow2(1n+d), hc, N.lt_le(SC.pow2(d), SC.pow2(1n+d), N.pow2_lt_succ(d)))
  +hn1 = N.le_lt_trans(SC.length(M.Node<K>, xs), SC.pow2(d), SC.pow2(1n+d), hc, N.pow2_lt_succ(d))
  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Bool, Nat.is_lt(d, l), True{}, hdl) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, False{}, _) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), Array.new(Nat, d, 0n)}, AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), NF.tag_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))), U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), Array.new(Nat, d, 0n)}, AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), NF.left_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))), U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), Array.new(Nat, d, 0n)}, AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), NF.right_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))), U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Nat>, ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), Array.new(Nat, d, 0n)}, AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)), NF.parent_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), _, M.ns_grow_keys(~K, d, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))), U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Array<Maybe<&2, K>>, ANode{AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), Array.new(Maybe<&2, K>, d, None{})}, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, NR.keys(~K, xs), None{})), NF.key_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)), _, U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  Equal.cong(M.NodeStore<K>, M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, z => (z, Done{Unit{}}), M.ns_put(~K, l, 1n+d, SC.pow2(1n+d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), x), NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), push_at(~K, l, 1n+d, xs, hl, hd1, hc1, x, hn1))

# full at the limit: nothing changes
def ns_push_full(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == False{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  %Equal.sym(Bool, Nat.is_lt(d, l), False{}, hdl) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, False{}, _) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
  {==}

# ---- clear ----


def drop_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(m), M.ntag(~K, M.Free{0n})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), NF.tag_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(m), M.nleft(~K, M.Free{0n})), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(m), M.nright(~K, M.Free{0n})), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(m), M.nleft(~K, M.Free{0n})), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), NF.left_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(m), M.nright(~K, M.Free{0n})), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(m), M.nright(~K, M.Free{0n})), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), NF.right_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})), Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), NF.parent_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), _, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n})), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})), NF.key_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), _} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
  %Equal.sym(Nat, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), m, len_init(M.Node<K>, xs, m, hm)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}))} : M.NodeStore<K>}
  {==}

def dr(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, m) == mv : Maybe<&2, M.Node<K>>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
  match mv:
    case None{}:
      +hi = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, 1n+m, SC.length(M.Node<K>, xs), Equal.sym(Nat, SC.length(M.Node<K>, xs), 1n+m, hm), N.lt_succ(m))
      Empty.absurd({M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, m), None{}, hmv, nth_isj(M.Node<K>, xs, m, hi))))
    case Some{+y0}:
      drop_some(~K, l, d, xs, hl, hd, hc, m, hm, y0, hmv)

# dropping the last live slot: the list without its last node
def ns_drop_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
  dr(~K, l, d, xs, hl, hd, hc, m, hm, SC.nth(M.Node<K>, xs, m), {==})

def clr(~K: Data, +k: Nat, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +hk: {SC.length(M.Node<K>, xs) == k : Nat}) -> {M.ns_clear_go(~K, k, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}:
  match k:
    case 0n:
      Equal.cong(List<&2, M.Node<K>>, M.NodeStore<K>, z => NR.real(~K, l, d, z), xs, Nil{}, LL.length_zero_nil(M.Node<K>, xs, hk))
    case 1n+ +m:
      +hm2 = len_init(M.Node<K>, xs, m, hk)
      %Equal.sym(M.NodeStore<K>, M.ns_drop(~K, NR.real(~K, l, d, xs), m), NR.real(~K, l, d, SC.init(M.Node<K>, xs)), ns_drop_ok(~K, l, d, xs, hl, hd, hc, m, hk)) : {M.ns_clear_go(~K, m, _) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}
      clr(~K, m, l, d, SC.init(M.Node<K>, xs), hl, hd, N.le_trans(SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), 1n+m, SC.pow2(d), L.subst(Nat, z => {Nat.is_le(z, 1n+m) == True{} : Bool}, m, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), Equal.sym(Nat, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), m, hm2), N.le_succ(m)), L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), 1n+m, hk, hc)), hm2)

# clear empties the list, keeping the capacity
def ns_clear_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_clear(~K, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}:
  clr(~K, SC.length(M.Node<K>, xs), l, d, xs, hl, hd, hc, {==})

# ---- reading one field of a slot ----


def ors(-X: Data, m: Maybe<&2, X>, +dv: X) -> X:
  match m:
    case None{}:
      dv
    case Some{x}:
      x

def nth_or_some(-X: Data, +xs: List<&2, X>, +i: Nat, +y: X, +dv: X, +h: {SC.nth(X, xs, i) == Some{y} : Maybe<&2, X>}) -> {ST.nth_or(X, xs, i, dv) == y : X}:
  match xs i:
    case Nil{} _:
      Empty.absurd({dv == y : X}, L.false_true(Equal.cong(Maybe<&2, X>, Bool, z => isj(X, z), None{}, Some{y}, h)))
    case Con{+x, r} 0n:
      Equal.cong(Maybe<&2, X>, X, z => ors(X, z, x), Some{x}, Some{y}, h)
    case Con{x, +r} 1n+q:
      nth_or_some(X, r, q, y, dv, h)

def nth_or_hi(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, xs, i, dv) == dv : X}:
  match xs i:
    case Nil{} _:
      {==}
    case Con{x, t} 0n:
      Empty.absurd({x == dv : X}, L.true_false(h))
    case Con{x, +t} 1n+q:
      nth_or_hi(X, t, q, dv, h)

def tag_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, _)) : M.NodeStore<K> & Nat}
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, y)), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_tag_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.ntag(~K, y)) : M.NodeStore<K> & Nat}
      {==}

def tag_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match b:
    case True{}:
      tag_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.ntag(~K, _)) : M.NodeStore<K> & Nat}
      {==}

# the field of the list's node (of Free{0} past the length)
def tag_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_tag_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  tag_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def left_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, _)) : M.NodeStore<K> & Nat}
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), M.nleft(~K, y)), NF.left_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_left_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nleft(~K, y)) : M.NodeStore<K> & Nat}
      {==}

def left_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match b:
    case True{}:
      left_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nleft(~K, _)) : M.NodeStore<K> & Nat}
      {==}

# the field of the list's node (of Free{0} past the length)
def left_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_left_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  left_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def right_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, _)) : M.NodeStore<K> & Nat}
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), M.nright(~K, y)), NF.right_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_right_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nright(~K, y)) : M.NodeStore<K> & Nat}
      {==}

def right_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match b:
    case True{}:
      right_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nright(~K, _)) : M.NodeStore<K> & Nat}
      {==}

# the field of the list's node (of Free{0} past the length)
def right_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_right_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  right_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def parent_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, _)) : M.NodeStore<K> & Nat}
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.nparent(~K, y)), NF.parent_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_parent_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nparent(~K, y)) : M.NodeStore<K> & Nat}
      {==}

def parent_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  match b:
    case True{}:
      parent_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nparent(~K, _)) : M.NodeStore<K> & Nat}
      {==}

# the field of the list's node (of Free{0} past the length)
def parent_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_parent_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
  parent_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})


# ---- writing one field of a slot ----

def isn(~K: Data, n: M.Node<K>) -> Bool:
  match n:
    case M.Free{x}:
      False{}
    case M.N{c, lf, rt, pa, k}:
      True{}

# a live node is below the length
def nth_or_lt(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +hn: {isn(~K, y) == True{} : Bool}, +h: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == y : M.Node<K>}) -> {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}:
  match xs i:
    case Nil{} _:
      Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.false_true(L.subst(M.Node<K>, z => {isn(~K, z) == True{} : Bool}, y, M.Free{0n}, Equal.sym(M.Node<K>, M.Free{0n}, y, h), hn)))
    case Con{x, r} 0n:
      {==}
    case Con{x, +r} 1n+q:
      nth_or_lt(~K, r, q, y, hn, h)

def nth_of_or(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == True{} : Bool}) -> {SC.nth(X, xs, i) == Some{ST.nth_or(X, xs, i, dv)} : Maybe<&2, X>}:
  match xs i:
    case Nil{} _:
      Empty.absurd({SC.nth(X, Nil{}, i) == Some{dv} : Maybe<&2, X>}, N.lt_zero_absurd(i, h))
    case Con{x, r} 0n:
      {==}
    case Con{x, +r} 1n+q:
      nth_of_or(X, r, q, dv, h)

def red_tag_eq(~K: Data, +v: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K) -> {M.ns_red_tag(v) == M.ntag(~K, M.N{v, lf, rt, q, k}) : Nat}:
  match v:
    case True{}:
      {==}
    case False{}:
      {==}

def left_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}:
  match c:
    case True{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}
    case False{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}

# writing the field of a live node: the list with that field replaced
def left_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}:
  +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
  +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}
  left_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)

def left_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  match b:
    case False{}:
      {==}
    case True{}:
      +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
      {==}

# writing the field of a free slot (or past the length) changes nothing
def left_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  left_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def right_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}:
  match c:
    case True{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}
    case False{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}

# writing the field of a live node: the list with that field replaced
def right_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}:
  +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
  +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}
  right_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)

def right_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  match b:
    case False{}:
      {==}
    case True{}:
      +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
      {==}

# writing the field of a free slot (or past the length) changes nothing
def right_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  right_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def parent_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}:
  match c:
    case True{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), _, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}
    case False{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), _, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}

# writing the field of a live node: the list with that field replaced
def parent_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}:
  +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
  +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}
  parent_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)

def parent_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  match b:
    case False{}:
      {==}
    case True{}:
      +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
      {==}

# writing the field of a free slot (or past the length) changes nothing
def parent_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  parent_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

def red_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}:
  match c:
    case True{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Nat, M.ns_red_tag(v), M.ntag(~K, M.N{v, lf, rt, q, k}), red_tag_eq(~K, v, lf, rt, q, k)) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), _), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}
    case False{}:
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Nat, M.ns_red_tag(v), M.ntag(~K, M.N{v, lf, rt, q, k}), red_tag_eq(~K, v, lf, rt, q, k)) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), _), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
      %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
      %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
      {==}

# writing the field of a live node: the list with that field replaced
def red_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}:
  +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
  +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
  %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
  red_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)

def red_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  match b:
    case False{}:
      {==}
    case True{}:
      +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
      %Equal.sym(Array<Nat> & Nat, Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)), (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
      {==}

# writing the field of a free slot (or past the length) changes nothing
def red_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
  red_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})

# ---- reading a slot's key ----

def key_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
  match mv:
    case None{}:
      Empty.absurd({M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
    case Some{+y}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, _)) : M.NodeStore<K> & Maybe<&2, K>}
      %Equal.sym(Array<Maybe<&2, K>> & Maybe<&2, K>, Array.get(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i)), (AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), M.nkey(~K, y)), NF.key_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_key_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), _) == (NR.real(~K, l, d, xs), M.nkey(~K, y)) : M.NodeStore<K> & Maybe<&2, K>}
      {==}

def key_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
  match b:
    case True{}:
      key_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
    case False{}:
      %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nkey(~K, _)) : M.NodeStore<K> & Maybe<&2, K>}
      {==}

# the key of the list's node (None for a free slot or past the length)
def key_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat) -> {M.ns_key_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
  key_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})