...

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index b644c4f42bf4443e616510164d7741dd90b054c1..c32d194363d282e57148a028257b1a215f230ba6 100644 (file)
--- 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. 
 
 (*