theorem sappeq2 (F: set) (_x1 _x2: nat): $ _x1 = _x2 -> F @@ _x1 == F @@ _x2 $;
_x1 = _x2 -> _x1 = _x2
_x1 = _x2 -> F @@ _x1 == F @@ _x2