find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → t
find env next exit = find-c (vart env) env next exit where
    find-c : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → 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 ¬b ¬c = find-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit
    ... | tri≈ ¬a b ¬c = exit record env {vart = n}
    ... | tri> ¬a ¬b c = find-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit