theorem writeeq1 (_F1 _F2: set) (a b: nat): $ _F1 == _F2 -> write _F1 a b == write _F2 a b $;
_F1 == _F2 -> _F1 == _F2
_F1 == _F2 -> write _F1 a b == write _F2 a b