module examplePostulate2 where


postulate A : Set
postulate B : Set
postulate f : A -> B
postulate a : A
postulate a' : A

b : B
b = f a

g : A -> A
g a = a