We wish to show that allow non-positive occurences of the inductive type in its constructor can lead to contradiction. Proof as haskell file below:

{-# LANGUAGE GADTs #-}data Void wheredata F where  FnSpace :: (F -> Void) -> Fcontra :: F -> Voidcontra f@(FnSpace fn) = fn finhab :: Finhab = FnSpace contra