-notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
-notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
-interpretation "Universal image ⊩⎻*" 'box x = (or_f_minus_star _ _ (rel x)).
-
-notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
-notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
-interpretation "Existential image ⊩" 'diamond x = (or_f _ _ (rel x)).
-
-notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
-notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
-interpretation "Universal pre-image ⊩*" 'rest x = (or_f_star _ _ (rel x)).
-
-notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
-notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
-interpretation "Existential pre-image ⊩⎻" 'ext x = (or_f_minus _ _ (rel x)).
-
-definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)).
-intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†H));] qed.
-
-lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed.
-coercion xxx.
+definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
+intros; constructor 1;
+ [ apply (λx.□⎽b (Ext⎽b x));
+ | intros; apply (†(†e));]
+qed.