module exampleproofproplogic11 where

data ⊤ : Set where
  true : ⊤ 

data ⊥ : Set where



data Bool : Set where
  ff : Bool
  tt : Bool


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


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

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

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


record Lemma5aux (a : Bool) : Set  where
  field
    b : Bool
    ab : a == ¬Bool b

Lemma5 : Set 
Lemma5 = (a : Bool) -> Lemma5aux a


lemma5 : Lemma5
lemma5 ff = record {b = tt; ab = true}
lemma5 tt = record {b = ff; ab = true}