theorem coeq1 (_F1 _F2 G: set): $ _F1 == _F2 -> _F1 o> G == _F2 o> G $;
_F1 == _F2 -> _F1 == _F2
_F1 == _F2 -> _F1 o> G == _F2 o> G