theorem grecaux1eq2 (K: set) (_x1 _x2 z n: nat): $ _x1 = _x2 -> grecaux1 K _x1 z n = grecaux1 K _x2 z n $;
_x1 = _x2 -> _x1 = _x2
_x1 = _x2 -> grecaux1 K _x1 z n = grecaux1 K _x2 z n