findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
           → treeInvariant env ∧ stackInvariant env
           → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
findP env Cond exit = findP-c (vart env) env Cond exit where
    findP-c : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (env : Env A)
           → treeInvariant env ∧ stackInvariant env
           → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
    findP-c leaf env Cond exit = exit env Cond
    findP-c n@(node key-t value ltree rtree) env Cond exit with <-cmp key-t (varn env)
    ... | tri< a ¬b ¬c = findP-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} {!!} exit
    ... | tri≈ ¬a b ¬c = exit record env {vart = n} {!!}
    ... | tri> ¬a ¬b c = findP-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} {!!} exit