From 68cadaa38277ea16ce97b3ed24884420c19eac20 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Sep 2009 09:59:15 +0000 Subject: [PATCH] Experiment... --- helm/software/matita/nlibrary/logic/cprop.ma | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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; -- 2.39.2