From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 Sep 2009 09:59:15 +0000 (+0000)
Subject: Experiment...
X-Git-Tag: make_still_working~3430
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68cadaa38277ea16ce97b3ed24884420c19eac20;hp=e91e815449698c6f2595958f94cd06c10ba10398;p=helm.git

Experiment...
---

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index e18811da4..d857ba6a7 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -52,7 +52,14 @@ ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 K2)]##]
 nqed.
 
-unification hint 0 ≔ A,B ⊢ fun21 … and_morphism A B ≡ And A B.
+(*unification hint 0 ≔ A,B ⊢ 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.*)
+
 
 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  #A; #A'; #B; #H1; #H2;