{-# LANGUAGE EmptyCase #-}data Voidabsurd :: Void -> aabsurd v = case v oftype NOT x = x -> Voidtype FALSE x = x -> Voidtype 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) -> VoidlemNotFalse f = f $ Right $ \a -> f (Left a)lemFalseExplodes :: FALSE (LEM a) -> anything-- lemFalseExplodes :: LEM a -> VoidlemFalseExplodes lem = absurd (lemNotFalse lem)