\sorts {
        U;
}

\functions {
	U x;
	U y;
	U z;
}

\problem {
    x = y -> y = x
}