prefer coercion Type_OF_objs2.
+notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B).
+
(* qui la notazione non va *)
lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
intros;