\sorts {
	A;
	B;
}

\functions {
	A a;
	B b;
	B f(B);
	B g(A);
}


\problem {
	\forall A x; f(g(x)) = g(x)
      & b = g(a)
   -> f(f(b)) = f(g(a))
}