module exampleimplicationbool 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 ->Bool ff = ff
_  ->Bool _  = tt


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

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