-notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
-
-interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
-interpretation "formal relation" 'form_rel r = (form_rel __ r).
-
-definition relation_pair_equality:
- ∀o1,o2. equivalence_relation2 (relation_pair o1 o2).
+definition Orelation_pair_equality:
+ ∀o1,o2. equivalence_relation2 (Orelation_pair o1 o2).