X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fcprop.ma;h=0302264c690a7575a63cce643fd9940933d23a12;hb=23a000715f1d3961b1b4a7efcf1870772d9bec93;hp=d006599ed93b49ffdb42ab46f8d1edbccd9b993a;hpb=6678a28314d8878bb46d5de7b1060628f4930242;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index d006599ed..0302264c6 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "hints_declaration.ma".
 include "sets/setoids1.ma".
 
 ndefinition CPROP: setoid1.
@@ -25,7 +26,8 @@ ndefinition CPROP: setoid1.
         [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
 nqed.
 
-unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+alias symbol "hint_decl" = "hint_decl_CProp2".
+unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
 
 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
@@ -50,15 +52,13 @@ ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 K2)]##]
 nqed.
 
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
 
 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  #A; #A'; #B; #H1; #H2;
  napply (. ((#‡H1)‡H2^-1)); nnormalize;
 nqed.*)
 
-(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
-
 ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
  napply mk_binary_morphism1
   [ napply Or
@@ -70,9 +70,7 @@ ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 H)]##]
 nqed.
 
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
-
-(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B.
 
 ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  napply mk_binary_morphism1
@@ -80,4 +78,4 @@ ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
   | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
      [ napply (if … H2); napply H; napply (fi … H1); nassumption
      | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
-nqed.
\ No newline at end of file
+nqed.