theorem greceq1 (_z1 _z2: nat) (K F: set) (n k: nat): $ _z1 = _z2 -> grec _z1 K F n k = grec _z2 K F n k $;
_z1 = _z2 -> _z1 = _z2
_z1 = _z2 -> grec _z1 K F n k = grec _z2 K F n k