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