theorem grecaux1eq1 (_K1 _K2: set) (x z n: nat): $ _K1 == _K2 -> grecaux1 _K1 x z n = grecaux1 _K2 x z n $;
_K1 == _K2 -> _K1 == _K2
_K1 == _K2 -> grecaux1 _K1 x z n = grecaux1 _K2 x z n