LostTypeError.agda:23,34-36 x != y of type A when checking that the expression px has type P (box y)