From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 29 Sep 2009 14:06:40 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3419
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=533389aa3b960f04c04ab1982d6ae47cf2d265e9;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index b644c4f42..c32d19436 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -211,12 +211,11 @@ unification hint 1 ≔
     
 nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A →
  ∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
- #U; #A; #B; #H; #x; #y; #K; #K2;
- alias symbol "prop2" = "prop21".
-alias symbol "invert" = "setoid1 symmetry".
-napply (. (K^-1 ‡ (prop21 ??? (intersect_ok'' U) ???? H^-1 #))); STOP
- 
- napply (. K^-1‡(H^-1‡#)); nassumption;
+ #U; #A; #B; #H; #x; #y; #K; #K2; napply (. #‡(?));
+##[ nchange with (A ∩ B = ?);
+    napply (prop21 ??? (mk_binary_morphism1 … (λS,S'.S ∩ S') (prop21 … (intersect_ok' U))) A A B B ##);
+    #H; napply H;
+  nassumption;
 nqed. 
 
 (*