- CURRY_EXISTS_CONV (Term `?(x,y). x + y = y + x`);
> val it = |- (?(x,y). x + y = y + x) = ?x y. x + y = y + x : thm

- CURRY_EXISTS_CONV (Term `?((w,x),(y,z)). w+x+y+z = z+y+x+w`);
> val it =
    |- (?((w,x),y,z). w + x + y + z = z + y + x + w) =
       ?(w,x) (y,z). w + x + y + z = z + y + x + w : thm