theorem coeq2 (F _G1 _G2: set): $ _G1 == _G2 -> F o> _G1 == F o> _G2 $;
_G1 == _G2 -> _G1 == _G2
_G1 == _G2 -> F o> _G1 == F o> _G2