-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (pair S S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
- [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
- |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-definition subset ≝ λO:bishop_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 "Bishop subset" 'subset a b = (subset _ a b).
-
-notation < "s 2 \atop \neq" non associative with precedence 90
- for @{ 'square2 $s }.
-notation > "s 'square'" non associative with precedence 90
- for @{ 'square $s }.
-interpretation "bishop set square" 'square x = (square_bishop_set x).
-interpretation "bishop set square" 'square2 x = (square_bishop_set x).
-