nicer hints, 16.1->3 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 20942ecc89b450555bce720dd7710eb51105e617..9b352d4a4112dcab86e9b922343b67414301fa63 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -81,6 +81,7 @@ unification hint 0 ≔ A,B:CProp[0];
 (*-------------------------------------------------------------*) ⊢
   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.