many fixes to setoids for re, 16.1 almost done

[helm.git] / helm / software / matita / nlibrary / logic / cprop.ma

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 1efc042ff8765fe609132230ee1a6965975b1e77..20942ecc89b450555bce720dd7710eb51105e617 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -48,11 +48,13 @@ ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP C
   [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
-  (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
-  (prop11 … and_morphism)
-   A B ≡ And A B.
+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)
+(*-------------------------------------------------------------*) ⊢
+  fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
 
 (*
 naxiom daemon: False.
@@ -71,12 +73,14 @@ ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CP
   [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
-  (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
-  (prop11 … or_morphism)
-  A B ≡ Or A B.
-
+unification hint 0 ≔ A,B:CProp[0];
+  T ≟ CPROP,
+  MM ≟ mk_unary_morphism1 …
+       (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+         (prop11 … or_morphism)
+(*-------------------------------------------------------------*) ⊢
+  fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
+  
 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