§ Excluded middle is not false in intuitionistic logic

{-# LANGUAGE EmptyCase #-}

data Void
absurd :: Void -> a
absurd v = case v of
type NOT x = x -> Void
type FALSE x = x -> Void
type LEM x = Either x (NOT x)

type NOTFALSE a = NOT (FALSE a)
lemNotFalse :: NOTFALSE (LEM a)
-- lemNotFalse :: (LEM a -> Void) -> Void
-- lemNotFalse :: (Either a (a -> Void) -> Void) -> Void
lemNotFalse f = f $ Right $ \a -> f (Left a)

lemFalseExplodes :: FALSE (LEM a) -> anything
-- lemFalseExplodes :: LEM a -> Void
lemFalseExplodes lem = absurd (lemNotFalse lem)