false.idr

module false 

%default total

data V : Type where
  Lam : ({a : Type} -> a -> a) -> V
  
t : V
t = Lam id
  
bad : V -> a
bad (Lam f) = bad (f (Lam f))
  
false : Void
false = bad t