module exampleProofPropLogic1 where 


postulate A : Set
postulate B : Set

Lemma1 : Set 
Lemma1 = A -> (A -> B)-> B

lemma1       : Lemma1
lemma1 a a-b = {! !}