module examplenegbool2 where

data Bool : Set where
  tt : Bool
  ff : Bool


data ⊤ : Set where
  true : ⊤ 


data ⊥ : Set where

Atom : Bool -> Set
Atom tt = ⊤ 
Atom ff = ⊥ 


¬Bool : Bool -> Bool  
¬Bool tt = ff
¬Bool ff = tt 

¬ : Set -> Set
¬ A = A -> ⊥ 

Lemma : Set
Lemma = (b : Bool) -> Atom (¬Bool b) -> ¬ (Atom b)

lemma : Lemma
lemma tt () _
lemma ff _ ()