(* *)
(**************************************************************************)
-include "cprop_connectives.ma".
+include "datatypes/constructors.ma".
+include "logic/cprop_connectives.ma".
(* Definition 2.1 *)
record ordered_set: Type ≝ {
definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-notation "a \subseteq u" left associative with precedence 70
- for @{ 'subset $a $u }.
-interpretation "ordered set subset" 'subset a b = (os_subset _ a b).
+interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).