qed.
notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
-interpretation "map arrows 2" 'map_arrows F x = (fun12 _ _ (map_arrows2 _ _ F _ _) x).
+interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);