+notation > "B ⇒_\obt2 C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+notation "B ⇒\sub (\obt 2) C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+interpretation "'arrows2_OBT" 'arrows2_OBT A B = (arrows2 OBTop A B).
+
+