From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Jul 2008 17:01:14 +0000 (+0000)
Subject: more notation moved to core notation, unification of duplicated CProp connectives
X-Git-Tag: make_still_working~4925
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=80ea6f314e89d9d280338c41860cb04949319629;p=helm.git

more notation moved to core notation, unification of duplicated CProp connectives
---

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index 8cb77ec24..64ae4495d 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -23,9 +23,6 @@ record bishop_set: Type ≝ {
   bs_cotransitive: cotransitive ? bs_apart
 }.
 
-notation "hvbox(a break # b)" non associative with precedence 45 
-  for @{ 'apart $a $b}.
-  
 interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
 
 definition bishop_set_of_ordered_set: ordered_set → bishop_set.
@@ -41,9 +38,6 @@ qed.
 (* Definition 2.2 (2) *)
 definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
 
-notation "hvbox(a break \approx b)" non associative with precedence 45 
-  for @{ 'napart $a $b}.
-      
 interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). 
 
 lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
@@ -97,7 +91,7 @@ qed.
 
 definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
-interpretation "bishop set subset" 'subset a b = (bs_subset _ a b). 
+interpretation "bishop set subset" 'subseteq a b = (bs_subset _ a b). 
 
 definition square_bishop_set : bishop_set → bishop_set.
 intro S; apply (mk_bishop_set (S × S));
diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
deleted file mode 100644
index 93fbac9b2..000000000
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ /dev/null
@@ -1,120 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "logic/equality.ma".
-include "datatypes/constructors.ma".
-
-inductive Or (A,B:CProp) : CProp ≝
- | Left : A → Or A B
- | Right : B → Or A B.
-
-interpretation "constructive or" 'or x y = (Or x y).
-
-inductive Or3 (A,B,C:CProp) : CProp ≝
- | Left3 : A → Or3 A B C
- | Middle3 : B → Or3 A B C
- | Right3 : C → Or3 A B C.
-
-interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
-
-notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
-
-inductive Or4 (A,B,C,D:CProp) : CProp ≝
- | Left3 : A → Or4 A B C D
- | Middle3 : B → Or4 A B C D
- | Right3 : C → Or4 A B C D
- | Extra3: D → Or4 A B C D.
-
-interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
-
-notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
-
-inductive And (A,B:CProp) : CProp ≝
- | Conj : A → B → And A B.
- 
-interpretation "constructive and" 'and x y = (And x y).
-
-inductive And3 (A,B,C:CProp) : CProp ≝
- | Conj3 : A → B → C → And3 A B C.
-
-notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
- 
-interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
-
-inductive And4 (A,B,C,D:CProp) : CProp ≝
- | Conj4 : A → B → C → D → And4 A B C D.
-
-notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
- 
-interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
-
-inductive exT (A:Type) (P:A→CProp) : CProp ≝
-  ex_introT: ∀w:A. P w → exT A P.
-  
-notation "\ll term 19 a, break term 19 b \gg" 
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b = 
-  (ex_introT _ _ a b).
-
-interpretation "CProp exists" 'exists \eta.x = (exT _ x).
-
-notation "\ll term 19 a, break term 19 b \gg" 
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b = 
-  (ex_introT _ _ a b).
-
-
-definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
-definition pi2exT ≝ 
-  λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
-
-interpretation "exT \fst" 'pi1 = (pi1exT _ _).
-interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x).
-interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y).
-interpretation "exT \snd" 'pi2 = (pi2exT _ _).
-interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
-interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
-
-inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
-  ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
-
-definition pi1exT23 ≝
-  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
-definition pi2exT23 ≝
-  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
-
-interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
-interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _).   
-interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
-interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
-interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
-interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
-
-definition Not : CProp → Prop ≝ λx:CProp.x → False.
-
-interpretation "constructive not" 'not x = (Not x).
-  
-definition cotransitive ≝
- λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y. 
-
-definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x).
-
-definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
-
-definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
-
-definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
-
-definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
- 
diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 419a80369..124d9017c 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,8 +1,7 @@
 ordered_uniform.ma uniform.ma
-cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
-russell_support.ma cprop_connectives.ma nat/nat.ma
+russell_support.ma logic/cprop_connectives.ma nat/nat.ma
 lebesgue.ma property_exhaustivity.ma sandwich.ma
-ordered_set.ma cprop_connectives.ma
+ordered_set.ma logic/cprop_connectives.ma
 bishop_set.ma ordered_set.ma
 bishop_set_rewrite.ma bishop_set.ma
 sandwich.ma ordered_uniform.ma
@@ -16,9 +15,9 @@ models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_
 models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
 models/q_function.ma Q/q/qtimes.ma models/q_bars.ma
 models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-models/list_support.ma cprop_connectives.ma list/list.ma nat/le_arith.ma nat/minus.ma
-models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
-models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma cprop_connectives.ma
+models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/le_arith.ma nat/minus.ma
+models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
+models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma
 models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
 models/q_shift.ma 
 models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
@@ -28,7 +27,7 @@ Q/q/qplus.ma
 Q/q/qtimes.ma 
 datatypes/constructors.ma 
 list/list.ma 
-logic/equality.ma 
+logic/cprop_connectives.ma 
 nat/compare.ma 
 nat/le_arith.ma 
 nat/minus.ma 
diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png
index 4fb8e3fd7..8633225a3 100644
Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ
diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma
index 4a335e01e..ea701bb9d 100644
--- a/helm/software/matita/contribs/dama/dama/models/list_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma
@@ -171,7 +171,7 @@ intros 2; elim n;
         |1: rewrite < H2; rewrite > len_append; rewrite > plus_n_SO; reflexivity]]]
 qed.
 
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 definition eject_N ≝
   λP.λp:∃x:nat.P x.match p with [ex_introT p _ ⇒ p].
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index b5610cbe0..5cf875f80 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -22,10 +22,10 @@ alias symbol "leq" = "natural 'less or equal to'".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); 
+intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
 fold normalize X; intros; cases H1; 
 alias symbol "plus" = "natural plus".
-alias symbol "nat" = "Uniform space N".
+alias symbol "N" = "Uniform space N".
 alias symbol "and" = "logical and".
 letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); 
 (* s - aj <= max 0 (u - i) *)  
@@ -116,7 +116,7 @@ qed.
 
 alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
-alias symbol "nat" = "ordered set N".
+alias symbol "N" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
index 5291a23fd..17fef4165 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma
@@ -25,4 +25,4 @@ lapply (H12 H1) as H13; apply (le_le_eq);
 |2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
 qed. 
  
-interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space.
+interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma
index cffccb59e..0b2d43563 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma
@@ -19,4 +19,4 @@ definition nat_uniform_space: uniform_space.
 apply (discrete_uniform_space_of_bishop_set ℕ);
 qed.
 
-interpretation "Uniform space N" 'nat = nat_uniform_space.
\ No newline at end of file
+interpretation "Uniform space N" 'N = nat_uniform_space.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
index 7279fe8c0..de3958907 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -15,7 +15,7 @@
 include "nat_ordered_set.ma".
 include "models/q_support.ma".
 include "models/list_support.ma". 
-include "cprop_connectives.ma". 
+include "logic/cprop_connectives.ma". 
 
 definition bar ≝ ℚ × (ℚ × ℚ).
 
diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma
index 6694a033f..70b3e6ade 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -14,10 +14,9 @@
 
 include "Q/q/qtimes.ma".
 include "Q/q/qplus.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
-notation "\rationals" non associative with precedence 99 for @{'q}.
-interpretation "Q" 'q = Q. 
+interpretation "Q" 'Q = Q. 
 
 (* group over Q *)
 axiom qp : ℚ → ℚ → ℚ.
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 23865418c..231cdf941 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -49,8 +49,7 @@ apply (mk_ordered_set ? nat_excess);
 |2: apply nat_excess_cotransitive]
 qed.
 
-notation "\naturals" non associative with precedence 90 for @{'nat}.
-interpretation "ordered set N" 'nat = nat_ordered_set.
+interpretation "ordered set N" 'N = nat_ordered_set.
 
 alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
 lemma os_le_to_nat_le:
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a227af3c1..45a8a1b37 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 (* Definition 2.1 *)
 record ordered_set: Type ≝ {
@@ -70,7 +70,5 @@ interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 
 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). 
 
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 66bcf6f0b..51ecff3f3 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -85,7 +85,7 @@ lemma invert_restriction_agreement:
   ∀O:ordered_uniform_space.∀l,r:O.
    ∀U:{[l,r]} square → Prop.∀u:O square → Prop.
     restriction_agreement ? l r U u →
-    restriction_agreement ? l r (inv U) (inv u).
+    restriction_agreement ? l r (\inv U) (\inv u).
 intros 9; split; intro;
 [1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);
 |2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);]
@@ -96,8 +96,10 @@ lemma bs_of_ss:
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝ 
   λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
 
+(*
 notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
+*)
 
 lemma ss_of_bs: 
  ∀O:ordered_set.∀u,v:O.
@@ -105,8 +107,10 @@ lemma ss_of_bs:
  λO:ordered_set.λu,v:O.
   λb:(O:bishop_set) square.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉.
 
+(*
 notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
 interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
+*)
 
 lemma segment_ordered_uniform_space: 
   ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
diff --git a/helm/software/matita/contribs/dama/dama/russell_support.ma b/helm/software/matita/contribs/dama/dama/russell_support.ma
index bcaabd677..deb5fc950 100644
--- a/helm/software/matita/contribs/dama/dama/russell_support.ma
+++ b/helm/software/matita/contribs/dama/dama/russell_support.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "nat/nat.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 definition hide ≝ λT:Type.λx:T.x.
 
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index f0260471f..6fa8e35ad 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -93,15 +93,15 @@ definition strictly_increasing ≝
 definition strictly_decreasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
 
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 50 
+notation > "s 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
 interpretation "Ordered set strict increasing"  'strictly_increasing s    = 
   (strictly_increasing _ s).
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 50 
+notation > "s 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
   (strictly_decreasing _ s).
@@ -229,10 +229,10 @@ interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
 (* Definition 2.8 *)
 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
-notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
+notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
 interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
 
-notation "hvbox(x \in break [a,b])" non associative with precedence 45 
+notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45 
   for @{'segment_in $a $b $x}.
 interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 82278eb08..a89a42ba8 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -14,7 +14,6 @@
 
 include "supremum.ma".
 
-
 (* Definition 2.13 *)
 alias symbol "square" = "bishop set square".
 alias symbol "pair" = "Pair construction".
@@ -34,11 +33,8 @@ interpretation "ordered set relations composition" 'compose a b = (compose_os_re
 definition invert_bs_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈\snd x,\fst x〉.
-    
-notation < "s \sup (-1)"  with precedence 70 for @{ 'invert $s }.
-notation < "s \sup (-1) x"  with precedence 70
-  for @{ 'invert_appl $s $x}. 
-notation > "'inv'" with precedence 70 for @{ 'invert_symbol  }.
+      
+notation > "\inv" with precedence 60 for @{ 'invert_symbol  }.
 interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
@@ -57,7 +53,7 @@ record uniform_space : Type ≝ {
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
   us_phi3: ∀U:us_carr square → Prop. us_unifbase U → 
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
-  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
+  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
 }.
 
 (* Definition 2.14 *)  
@@ -66,9 +62,9 @@ definition cauchy ≝
   λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → 
    ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
    
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 
+notation < "a \nbsp 'is_cauchy'" non associative with precedence 45 
   for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 50 
+notation > "a 'is_cauchy'" non associative with precedence 45 
   for @{'cauchy $a}.
 interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
    
@@ -77,9 +73,9 @@ definition uniform_converge ≝
   λC:uniform_space.λa:sequence C.λu:C.
     ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U 〈u,a i〉.
     
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
+notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
   for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 50 
+notation > "a 'uniform_converges' x" non associative with precedence 45 
   for @{'uniform_converge $a $x}.
 interpretation "Uniform convergence" 'uniform_converge s u =
  (uniform_converge _ s u).
diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index ed0c7007b..b201a0555 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -94,6 +94,10 @@ notation "hvbox(a break * b)"
   left associative with precedence 55
 for @{ 'times $a $b }.
 
+notation "hvbox(a break \middot b)" 
+  left associative with precedence 55
+  for @{ 'middot $a $b }.
+
 notation "hvbox(a break \mod b)" 
   left associative with precedence 55
 for @{ 'module $a $b }.
@@ -117,10 +121,6 @@ notation "a !"
   non associative with precedence 80
 for @{ 'fact $a }.
 
-notation "(a \sup b)"
-  right associative with precedence 65
-for @{ 'exp $a $b}.
-
 notation "\sqrt a" 
   non associative with precedence 60
 for @{ 'sqrt $a }.
@@ -136,3 +136,52 @@ for @{ 'and $a $b }.
 notation "hvbox(\lnot a)" 
   non associative with precedence 40
 for @{ 'not $a }.
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" non associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.
+        
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.
+    
+notation "hvbox(a break \circ b)" 
+  left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
+notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}. 
+
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index aeb0d779a..29324c4aa 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -33,11 +33,7 @@ record Group : Type ≝
    group_properties:> isGroup pregroup
  }.
 
-notation "hvbox(x \sup (-1))" with precedence 89
-for @{ 'ginv $x }.
-
-interpretation "Group inverse" 'ginv x =
- (cic:/matita/algebra/groups/inv.con _ x).
+interpretation "Group inverse" 'invert x = (inv _ x).
 
 definition left_cancellable ≝
  λT:Type. λop: T -> T -> T.
@@ -88,7 +84,7 @@ reflexivity.
 qed.
 
 theorem eq_opxy_e_to_eq_x_invy:
- ∀G:Group. ∀x,y:G. x·y=1 → x=y \sup -1.
+ ∀G:Group. ∀x,y:G. x·y=ⅇ → x=y \sup -1.
 intros;
 apply (eq_op_x_y_op_z_y_to_eq ? y);
 rewrite > (inv_is_left_inverse ? G);
@@ -96,7 +92,7 @@ assumption.
 qed.
 
 theorem eq_opxy_e_to_eq_invx_y:
- ∀G:Group. ∀x,y:G. x·y=1 → x \sup -1=y.
+ ∀G:Group. ∀x,y:G. x·y=ⅇ → x \sup -1=y.
 intros;
 apply (eq_op_x_y_op_x_z_to_eq ? x);
 rewrite > (inv_is_right_inverse ? G);
@@ -140,20 +136,14 @@ qed.
 (* Morphisms *)
 
 record morphism (G,G':Group) : Type ≝
- { image: G → G';
+ { image:1> G → G';
    f_morph: ∀x,y:G.image(x·y) = image x · image y
  }.
  
-notation "hvbox(f\tilde x)" with precedence 79
-for @{ 'morimage $f $x }.
-
-interpretation "Morphism image" 'morimage f x =
- (cic:/matita/algebra/groups/image.con _ _ f x).
- 
 theorem morphism_to_eq_f_1_1:
- ∀G,G'.∀f:morphism G G'.f˜1 = 1.
+ ∀G,G'.∀f:morphism G G'.f ⅇ  = ⅇ.
 intros;
-apply (eq_op_x_y_op_z_y_to_eq ? (f˜1));
+apply (eq_op_x_y_op_z_y_to_eq ? (f ⅇ));
 rewrite > (e_is_left_unit ? G');
 rewrite < f_morph;
 rewrite > (e_is_left_unit ? G);
@@ -162,9 +152,9 @@ qed.
  
 theorem eq_image_inv_inv_image:
  ∀G,G'.∀f:morphism G G'.
-  ∀x.f˜(x \sup -1) = (f˜x) \sup -1.
+  ∀x.f (x \sup -1) = (f x) \sup -1.
 intros;
-apply (eq_op_x_y_op_z_y_to_eq ? (f˜x));
+apply (eq_op_x_y_op_z_y_to_eq ? (f x));
 rewrite > (inv_is_left_inverse ? G');
 rewrite < f_morph;
 rewrite > (inv_is_left_inverse ? G);
diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index 556faf6ca..fe35eeb67 100644
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/matita/library/algebra/monoids.ma
@@ -32,21 +32,17 @@ record Monoid : Type ≝
    monoid_properties:> isMonoid premonoid 
  }.
 
-notation "1" with precedence 89
-for @{ 'munit }.
-
-interpretation "Monoid unit" 'munit =
- (cic:/matita/algebra/monoids/e.con _).
+interpretation "Monoid unit" 'neutral = (e _).
   
 definition is_left_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. (opp x)·x = 1.
+   ∀x:M. (opp x)·x = ⅇ.
    
 definition is_right_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. x·(opp x) = 1.
+   ∀x:M. x·(opp x) = ⅇ.
 
 theorem is_left_inverse_to_is_right_inverse_to_eq:
  ∀M:Monoid. ∀l,r.
diff --git a/helm/software/matita/library/algebra/semigroups.ma b/helm/software/matita/library/algebra/semigroups.ma
index 5a739ae12..af5e01e06 100644
--- a/helm/software/matita/library/algebra/semigroups.ma
+++ b/helm/software/matita/library/algebra/semigroups.ma
@@ -21,12 +21,7 @@ record Magma : Type≝
    op: carrier → carrier → carrier
  }.
 
-notation "hvbox(a break \middot b)" 
-  left associative with precedence 55
-for @{ 'magma_op $a $b }.
-
-interpretation "magma operation" 'magma_op a b =
- (cic:/matita/algebra/semigroups/op.con _ a b).
+interpretation "magma operation" 'middot a b = (op _ a b).
 
 (* Semigroups *)
 
diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
new file mode 100644
index 000000000..f9fae64a0
--- /dev/null
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/cprop_connectives.ma".
+
+record powerset (A: Type) : Type ≝ { char: A → CProp }.
+
+interpretation "powerset" 'powerset A = (powerset A).
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+
+definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
+
+interpretation "mem" 'mem a S = (mem _ S a).
+
+definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
+
+interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
+
+definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
+
+interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
+
+definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
+
+interpretation "intersects" 'intersects U V = (intersects _ U V).
+
+definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
+
+interpretation "union" 'union U V = (union _ U V).
+
+include "logic/equality.ma".
+
+definition singleton ≝ λA:Type.λa:A.{b | a=b}.
+
+interpretation "singleton" 'singl a = (singleton _ a).
diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index a68378408..3814ac3f1 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -12,82 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/equality.ma".
-
-inductive And (A,B:CProp) : CProp ≝
- conj: A → B → And A B.
- 
-interpretation "constructive and" 'and x y = (And x y).
-
-inductive Or (A,B:CProp) : CProp ≝
- | or_intro_l: A → Or A B
- | or_intro_r: B → Or A B. 
- 
-interpretation "constructive or" 'or x y = (Or x y).
-
-inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
-  ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
-
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
-
-notation "hvbox(2 \sup A)" non associative with precedence 45
-for @{ 'powerset $A }.
-
-interpretation "powerset" 'powerset A = (powerset A).
-
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
-
-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-notation "hvbox(a break ∪ b)" non associative with precedence 55
-for @{ 'union $a $b }. (* \cup *)
-
-interpretation "union" 'union U V = (union _ U V).
+include "datatypes/subsets.ma".
 
 record axiom_set : Type ≝ { 
   A:> Type;
   i: A → Type;
-  C: ∀a:A. i a → 2 \sup A
+  C: ∀a:A. i a → Ω \sup A
 }.
 
-inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
+inductive for_all (A: axiom_set) (U,V: Ω \sup A) (covers: A → CProp) : CProp ≝
    iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
 
-inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+inductive covers (A: axiom_set) (U: \Omega \sup A) : A → CProp ≝
    refl: ∀a:A. a ∈ U → covers A U a
  | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
 
@@ -98,8 +34,8 @@ interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
 interpretation "covers" 'covers a U = (covers _ U a).
 
 definition covers_elim ≝
- λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
-  λH1:∀a:A. a ∈ U → a ∈ P.
+ λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
+  λH1: U ⊆ P. 
    λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
     let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
      match p return λaa.λ_:aa ◃ U.aa ∈ P with
@@ -111,10 +47,10 @@ definition covers_elim ≝
     in
      aux.
 
-inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
+inductive ex_such (A : axiom_set) (U,V : \Omega \sup A) (fish: A → CProp) : CProp ≝
  found : ∀a. a ∈ V → fish a → ex_such A U V fish.
 
-coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
+coinductive fish (A:axiom_set) (U: \Omega \sup A) : A → CProp ≝
  mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
@@ -123,8 +59,8 @@ for @{ 'fish $a $b }. (* a \ltimes b *)
 interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
 interpretation "fish" 'fish a U = (fish _ U a).
 
-let corec fish_rec (A:axiom_set) (U: 2 \sup A)
- (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
+let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
+ (P: Ω \sup A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
@@ -177,12 +113,6 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
     cases (H1 i); clear H1; apply (H3 a1); assumption]
 qed.
 
-definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}.
-
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
-interpretation "singleton" 'singl a = (singleton _ a).
-
 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
 
 interpretation "covered by one" 'leq a b = (leq _ a b).
@@ -211,13 +141,13 @@ notation "↑a" with precedence 80 for @{ 'uparrow $a }.
 
 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 
-definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
 
 notation "↓a" with precedence 80 for @{ 'downarrow $a }.
 
 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 
-definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
 notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
 
@@ -225,6 +155,6 @@ interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
  }.
 
diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index bd27126af..2be7477f3 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -10,6 +10,7 @@ Z/z.ma datatypes/bool.ma nat/nat.ma
 datatypes/constructors.ma logic/equality.ma
 datatypes/compare.ma 
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
+datatypes/subsets.ma logic/cprop_connectives.ma logic/equality.ma
 algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
 algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
 algebra/semigroups.ma higher_order_defs/functions.ma
@@ -17,7 +18,8 @@ algebra/monoids.ma algebra/semigroups.ma
 demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
 demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
 demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
-demo/formal_topology.ma logic/equality.ma
+demo/formal_topology.ma datatypes/subsets.ma
+demo/natural_deduction.ma 
 list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
 list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
 list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
@@ -25,6 +27,7 @@ logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
 logic/connectives.ma 
 logic/coimplication.ma logic/connectives.ma
 logic/connectives2.ma higher_order_defs/relations.ma
+logic/cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
 nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
 nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
diff --git a/helm/software/matita/library/higher_order_defs/functions.ma b/helm/software/matita/library/higher_order_defs/functions.ma
index a6174f48f..195cbfc17 100644
--- a/helm/software/matita/library/higher_order_defs/functions.ma
+++ b/helm/software/matita/library/higher_order_defs/functions.ma
@@ -18,10 +18,6 @@ definition compose \def
   \lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A.
   f (g x).
 
-notation "hvbox(a break \circ b)" 
-  left associative with precedence 70
-for @{ 'compose $a $b }.
-
 interpretation "function composition" 'compose f g =
   (cic:/matita/higher_order_defs/functions/compose.con _ _ _ f g).
 
diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma
new file mode 100644
index 000000000..b4c556d83
--- /dev/null
+++ b/helm/software/matita/library/logic/cprop_connectives.ma
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/equality.ma".
+include "datatypes/constructors.ma".
+
+inductive Or (A,B:CProp) : CProp ≝
+ | Left : A → Or A B
+ | Right : B → Or A B.
+
+interpretation "constructive or" 'or x y = (Or x y).
+
+inductive Or3 (A,B,C:CProp) : CProp ≝
+ | Left3 : A → Or3 A B C
+ | Middle3 : B → Or3 A B C
+ | Right3 : C → Or3 A B C.
+
+interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
+
+notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
+
+inductive Or4 (A,B,C,D:CProp) : CProp ≝
+ | Left3 : A → Or4 A B C D
+ | Middle3 : B → Or4 A B C D
+ | Right3 : C → Or4 A B C D
+ | Extra3: D → Or4 A B C D.
+
+interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
+
+notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
+
+inductive And (A,B:CProp) : CProp ≝
+ | Conj : A → B → And A B.
+ 
+interpretation "constructive and" 'and x y = (And x y).
+
+inductive And3 (A,B,C:CProp) : CProp ≝
+ | Conj3 : A → B → C → And3 A B C.
+
+notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
+ 
+interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
+
+inductive And4 (A,B,C,D:CProp) : CProp ≝
+ | Conj4 : A → B → C → D → And4 A B C D.
+
+notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
+ 
+interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
+
+inductive exT (A:Type) (P:A→CProp) : CProp ≝
+  ex_introT: ∀w:A. P w → exT A P.
+  
+notation "\ll term 19 a, break term 19 b \gg" 
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b = 
+  (ex_introT _ _ a b).
+
+interpretation "CProp exists" 'exists \eta.x = (exT _ x).
+
+notation "\ll term 19 a, break term 19 b \gg" 
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b = 
+  (ex_introT _ _ a b).
+
+
+definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
+definition pi2exT ≝ 
+  λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
+
+interpretation "exT \fst" 'pi1 = (pi1exT _ _).
+interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x).
+interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y).
+interpretation "exT \snd" 'pi2 = (pi2exT _ _).
+interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
+interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
+
+inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
+  ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+
+definition pi1exT23 ≝
+  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
+definition pi2exT23 ≝
+  λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
+
+interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
+interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _).   
+interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
+
+inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
+  ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
+
+definition Not : CProp → Prop ≝ λx:CProp.x → False.
+
+interpretation "constructive not" 'not x = (Not x).
+  
+definition cotransitive ≝
+ λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y. 
+
+definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x).
+
+definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+
+definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
+
+definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+
+definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+