theorem greceq3 (z: nat) (K _F1 _F2: set) (n k: nat): $ _F1 == _F2 -> grec z K _F1 n k = grec z K _F2 n k $;
_F1 == _F2 -> _F1 == _F2
_F1 == _F2 -> grec z K _F1 n k = grec z K _F2 n k