gistfile1.idr

total
isElem' : DecEq a => (e : a) -> (t : Tree a) -> Dec (IsElem e t)
isElem' x Leaf = No $ \p => noElemInLeaf x p
  where
    total
    noElemInLeaf : (x : a) -> IsElem x Leaf -> _|_
    noElemInLeaf x Here impossible

isElem' x (Branch l y r) with (decEq x y)
  isElem' x (Branch l x r) | Yes refl = Yes Here
  isElem' x (Branch l y r) | No nc with (isElem' x l)
    isElem' x (Branch l y r) | No nc | Yes p  = Yes $ IsLeft p
    isElem' x (Branch l y r) | No nc | No nl with (isElem' x r)
      isElem' x (Branch l y r) | No nc | No nl | Yes p  = Yes $ IsRight p
      isElem' x (Branch l y r) | No nc | No nl | No  nr =
        No $ \p => notInTree x y l r nc nl nr p
        where
          total
          notInTree : (x, y : a) ->
                      (l, r : Tree a) ->
                      (nc : x = y -> _|_) ->
                      (nl : IsElem x l -> _|_) ->
                      (nr : IsElem x r -> _|_) ->
                      (p : IsElem x (Branch l y r)) -> _|_
          notInTree x x l r nc nl nr Here        = nc refl
          notInTree x y l r nc nl nr (IsLeft  z) = nl z
          notInTree x y l r nc nl nr (IsRight z) = nr z