notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).