theorem greceq2 (z: nat) (_K1 _K2 F: set) (n k: nat): $ _K1 == _K2 -> grec z _K1 F n k = grec z _K2 F n k $;
_K1 == _K2 -> _K1 == _K2
_K1 == _K2 -> grec z _K1 F n k = grec z _K2 F n k