Intuitionist logic is by no means denying the law of excluded middle!

NotNotLEM.idr

module NotNotLEM

%default total
%access public export

notDistributesOverEither : Not (Either a b) -> (Not a, Not b)
notDistributesOverEither neither = (notLeft neither, notRight neither) where
  notLeft : Not (Either a b) -> Not a
  notLeft neither x = neither (Left x)

  notRight : Not (Either a b) -> Not b
  notRight nor y = nor (Right y)

notNotExcludedMiddle : Not (Not (Either a (Not a)))
notNotExcludedMiddle middle =
  let (notA, notNotA) = notDistributesOverEither middle
  in notNotA notA