theorem greceq4 (z: nat) (K F: set) (_n1 _n2 k: nat): $ _n1 = _n2 -> grec z K F _n1 k = grec z K F _n2 k $;
_n1 = _n2 -> _n1 = _n2
_n1 = _n2 -> grec z K F _n1 k = grec z K F _n2 k