package exampleSimpleEquality (A :: Type) (a:: A) (f:: A -> Type) where 

   g  (a:: A)
      :: A
      = a

   a' :: A
      = g a

   p  (x :: f a)
      :: (f a')
      = {! !}