X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fcprop.ma;h=e7ecf01ad5f47a49885a477b1b96138de00d893e;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=20942ecc89b450555bce720dd7710eb51105e617;hpb=2c486bbea1d6ffb072d0ff83f9df129b7860f3e1;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 20942ecc8..e7ecf01ad 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -50,9 +50,9 @@ nqed.
 
 unification hint 0 ≔ A,B:CProp[0];
   T ≟ CPROP,
-  MM ≟ mk_unary_morphism1 …
-       (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
-         (prop11 … and_morphism)
+  MM ≟ mk_unary_morphism1 ??
+       (λX.mk_unary_morphism1 ?? (And X) (prop11 ?? (fun11 ?? and_morphism X)))
+         (prop11 ?? and_morphism)
 (*-------------------------------------------------------------*) ⊢
   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
 
@@ -76,11 +76,12 @@ nqed.
 unification hint 0 ≔ A,B:CProp[0];
   T ≟ CPROP,
   MM ≟ mk_unary_morphism1 …
-       (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+       (λX.mk_unary_morphism1 … (Or X) (prop11 … (fun11 ?? or_morphism X)))
          (prop11 … or_morphism)
 (*-------------------------------------------------------------*) ⊢
   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
   
+(* XXX always applied, generates hard unif problems  
 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
  #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
@@ -88,12 +89,16 @@ ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CP
  //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
-  (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
-  (prop11 … if_morphism)
-  A B ≡ A → B.
-  
+unification hint 0 ≔ A,B:CProp[0];
+  T ≟ CPROP,
+  R ≟ mk_unary_morphism1 …
+       (λX:CProp[0].mk_unary_morphism1 … 
+         (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+         (prop11 … if_morphism)
+(*----------------------------------------------------------------------*) ⊢
+  fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R A) B ≡ A → B.
+*)
+
 (* not as morphism *)
 nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
 @(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
@@ -116,33 +121,35 @@ nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CP
 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P); 
 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
    B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P) 
-        (prop11 ?? (Ex_morphism S))
+   M ≟ mk_unary_morphism1 ?? 
+         (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (fun11 ?? P)) 
+         (prop11 ?? (Ex_morphism S))
 (*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (fun11 (setoid1_of_setoid S) CPROP P).
+  fun11 A B M P ≡ Ex (carr S) (fun11 (setoid1_of_setoid S) CPROP P).
 
 nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x)); 
 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
    B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x)) 
-        (prop11 ?? (Ex_morphism_eta S))
+   M ≟ mk_unary_morphism1 ?? 
+         (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (λx.fun11 ?? P x)) 
+         (prop11 ?? (Ex_morphism_eta S))
 (*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (λx.fun11 (setoid1_of_setoid S) CPROP P x).
+  fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).
 
 nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
 #T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
 
-unification hint 0 ≔ T,P ; 
+unification hint 0 ≔ T : setoid,P ; 
    S ≟ (Ex_setoid T P) 
 (*---------------------------*) ⊢
-   Ex T (λx:T.P x) ≡ carr S.
+   Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
 
 (* couts how many Ex we are traversing *)
 ninductive counter : Type[0] ≝