treeInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! Set
treeInvariant leaf = ⊤
treeInvariant (node key value leaf leaf) = ⊤
treeInvariant (node key value leaf n@(node key!$\text{1}$! value!$\text{1}$! t!$\text{1}$! t₂)) =  (key < key!$\text{1}$!) !$\wedge$! treeInvariant n
treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) leaf) =  treeInvariant n !$\wedge$! (key < key!$\text{1}$!)
treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n !$\wedge$!  (key < key!$\text{1}$!) !$\wedge$! (key!$\text{1}$! < key₂) !$\wedge$! treeInvariant m

stackInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (stack  : List (bt A)) !$\rightarrow$! Set n
stackInvariant {_} {A} _ [] = Lift _ ⊤
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$!