module exampleLessBool where


data Bool : Set where 
  tt : Bool
  ff : Bool


_<Bool_ : Bool -> Bool -> Bool
ff <Bool b = b 
tt <Bool _ = ff


_<Boollong_ : Bool -> Bool -> Bool
ff <Boollong ff = tt 
ff <Boollong tt = tt 
tt <Boollong ff = ff
tt <Boollong tt = ff

data ⊤ : Set where
  true : ⊤ 

data ⊥ : Set where


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

_<_ : Bool -> Bool -> Set
b < b' = Atom (b <Bool b')


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

Lemma4 : Set
Lemma4 = (a : Bool) -> ¬ (a < a)

lemma4 : Lemma4
lemma4 ff () 
lemma4 tt ()