From 533389aa3b960f04c04ab1982d6ae47cf2d265e9 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 29 Sep 2009 14:06:40 +0000
Subject: [PATCH] ...

---
 helm/software/matita/nlibrary/sets/sets.ma | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

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. 
 
 (*
-- 
2.39.2