theorem all2eq (_R1 _R2: set): $ _R1 == _R2 -> all2 _R1 == all2 _R2 $;
_R1 == _R2 -> _R1 == _R2
_R1 == _R2 -> all2 _R1 == all2 _R2