treeInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! Set
treeInvariant leaf = !$\top$!
treeInvariant (node key value leaf leaf) = !$\top$!
treeInvariant (node key value leaf n@(node key!$\_{1}$! value!$\_{1}$! t!$\_{1}$! t!$\_{2}$!)) =  (key < key!$\_{1}$!) !$\wedge$! treeInvariant n
treeInvariant (node key value n@(node key!$\_{1}$! value!$\_{1}$! t t!$\_{1}$!) leaf) =  treeInvariant n !$\wedge$! (key < key!$\_{1}$!)
treeInvariant (node key value n@(node key!$\_{1}$! value!$\_{1}$! t t!$\_{1}$!) m@(node key!$\_{2}$! value!$\_{2}$! t!$\_{2}$! t!$\_{3}$!)) = treeInvariant n !$\wedge$!  (key < key!$\_{1}$!) !$\wedge$! (key!$\_{1}$! < key!$\_{2}$!) !$\wedge$! treeInvariant m

stackInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (stack  : List (bt A)) !$\rightarrow$! Set n
stackInvariant {_} {A} _ [] = Lift _ !$\top$!
stackInvariant {_} {A} tree (tree1 !$\text{::}$! [] ) = tree1 !$\equiv$! tree
stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value leaf right !$\text{::}$! _) ) = (right !$\equiv$! x) !$\wedge$! stackInvariant tree tail
stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value left leaf !$\text{::}$! _) ) = (left !$\equiv$! x) !$\wedge$! stackInvariant tree tail
stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value left right !$\text{::}$! _  )) = ( (left !$\equiv$! x) !$\wedge$! stackInvariant tree tail) ∨ ( (right !$\equiv$! x) !$\wedge$! stackInvariant tree tail)
stackInvariant {_} {A} tree s = Lift _ !$\bot$!