theorem coeq1d (_G: wff) (_F1 _F2 G: set): $ _G -> _F1 == _F2 $ > $ _G -> _F1 o> G == _F2 o> G $;
_G -> _F1 == _F2
_G -> G == G
_G -> _F1 o> G == _F2 o> G