interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans" 'trans r = (trans ????? r).
intros; apply (if ?? H); assumption.
qed.
-notation ". r" with precedence 50 for @{'if $r}.
+notation ". r" with precedence 55 for @{'if $r}.
interpretation "if" 'if r = (if' ?? r).
definition and_morphism: binary_morphism1 CPROP CPROP CPROP.