theorem coeq2d (_G: wff) (F _G1 _G2: set): $ _G -> _G1 == _G2 $ > $ _G -> F o> _G1 == F o> _G2 $;
_G -> F == F
_G -> _G1 == _G2
_G -> F o> _G1 == F o> _G2