module exampleSimpleEquality2 where

postulate A : Set
postulate a : A
postulate P : A -> Set

g : A -> A
g a = a

a' : A
a' = g a

p : P a -> P a'
p x = x