(**************************************************************************)
include "formal_topology/cprop_connectives.ma".
+include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/invert_1.ma".
inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝
refl: eq A x x.
notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
-*)
\ No newline at end of file
+*)