def upd_perfect

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:202

import Base

202def upd_perfect(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, upd(T, d, t, j, v)) == True{} : Bool}:
203  tupd_perfect(T, d, t, j, v, ndec(d, j), pf)