treeInvariant : {n : Level} {A : Set n} → (tree : bt A) → Set
treeInvariant leaf = ⊤
treeInvariant (node key value leaf leaf) = ⊤
treeInvariant (node key value leaf n@(node key₁ value₁ t₁ t₂)) =  (key < key₁) ∧ treeInvariant n
treeInvariant (node key value n@(node key₁ value₁ t t₁) leaf) =  treeInvariant n ∧ (key < key₁)
treeInvariant (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n ∧  (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant m

stackInvariant : {n : Level} {A : Set n} → (tree : bt A) → (stack  : List (bt A)) → Set n
stackInvariant {_} {A} _ [] = Lift _ ⊤
stackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
stackInvariant {_} {A} tree (x ∷ tail @ (node key value leaf right ∷ _) ) = (right ≡ x) ∧ stackInvariant tree tail
stackInvariant {_} {A} tree (x ∷ tail @ (node key value left leaf ∷ _) ) = (left ≡ x) ∧ stackInvariant tree tail
stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail)
stackInvariant {_} {A} tree s = Lift _ ⊥