findP : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (env : Env A)
           !$\rightarrow$! treeInvariant env !$\wedge$! stackInvariant env
           !$\rightarrow$! (exit : (env : Env A) !$\rightarrow$! treeInvariant env !$\wedge$! stackInvariant env !$\rightarrow$! t ) !$\rightarrow$! t
findP env Cond exit = findP-c (vart env) env Cond exit where
    findP-c : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (env : Env A)
           !$\rightarrow$! treeInvariant env !$\wedge$! stackInvariant env
           !$\rightarrow$! (exit : (env : Env A) !$\rightarrow$! treeInvariant env !$\wedge$! stackInvariant env !$\rightarrow$! t ) !$\rightarrow$! 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 !$\neg$!b !$\neg$!c = findP-c ltree record env {vart = ltree ; varl = (n !$\text{::}$! (varl env))} {!!} exit
    ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = exit record env {vart = n} {!!}
    ... | tri> !$\neg$!a !$\neg$!b c = findP-c rtree record env {vart = rtree ; varl = (n !$\text{::}$! (varl env))} {!!} exit