theorem writeeq3 (F: set) (a _b1 _b2: nat): $ _b1 = _b2 -> write F a _b1 == write F a _b2 $;
_b1 = _b2 -> _b1 = _b2
_b1 = _b2 -> write F a _b1 == write F a _b2