LostTypeError2.agda:25,32-34 x != y of type A when checking that the expression Px has type P (box y)