proofs/containers/balanced_search_tree/rmv.bend checks

import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./ok.bend as OK
import ./reads.bend as RD
import ./find.bend as FI
import ./ends.bend as EN
import ./path.bend as P
import ./plug.bend as PG
import ./ord.bend as OR
import ./prim.bend as PR
import ./tree.bend as TR
import ./spath.bend as SP
import ../../lib/nat.bend as N
import ./alls.bend as AL
import ./dj.bend as DJ
import ./nbr.bend as NB
import ./xtr.bend as XT
import ./frame.bend as FRM
import ./succ.bend as SU
import ./unl.bend as UN
import ./rms.bend as RS
import ./rmd.bend as RMD
import ./putm.bend as PM
import ./dord.bend as DO
import ../../lib/nat_list.bend as NL