find : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (env : Env A )
           !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t )
           !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t
find env next exit = find-c (vart env) env next exit where
    find-c : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (env : Env A )
           !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t )
           !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t
    find-c leaf env next exit = exit env
    find-c n@(node key-t value ltree rtree) env next exit with <-cmp (varn env) key-t
    ... | tri< a !$\neg$!b !$\neg$!c = find-c ltree record env {vart = ltree ; varl = (n !$\text{::}$! (varl env))} next exit
    ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = exit record env {vart = n}
    ... | tri> !$\neg$!a !$\neg$!b c = find-c rtree record env {vart = rtree ; varl = (n !$\text{::}$! (varl env))} next exit