...

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index dcd9a226d3e5fb46b51fb23ad3c8d8bdded3020c..14d52373eebd3d4a37a518387def471d22438d08 100644 (file)
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -349,14 +349,16 @@ nqed.
 
 nlemma ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
 #T P; @ (Ex T (λx:T.P x)); @;
-##[ #H1 H2; ncases H1; ncases H2; #x Px y Py; napply (x = y);
-##| #H; napply (?:?); ncases H; nelim H;  nnormalize;
+##[ #H1 H2; napply True |##*: //; ##]
+nqed.
+
+unification hint 0 ≔ T,P ; S ≟ (ex_setoid T P) ⊢
+ Ex T (λx:T.P x) ≡ carr S.
 
 nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
  ∀x,y:setoid1_of_setoid S.x =_1 y → 
    ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
 #S m x y E;
-napply (. (? ‡ #));
 napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
 napply #.
 nqed.
@@ -372,20 +374,23 @@ ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
     nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
     nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
     napply (.= (#‡H2));
-    napply (. (?‡#)); 
-    nlapply (.=_1 (∑ E (λx,H.?))╪_1 #);
-    napply (.=_1 (∑ E (λx,H.#))╪_1 #);
-    
+    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))╪_1 #); ##[
+      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+      napply ( (X‡#)‡#); ##]
+    napply #;
+##| #e1 e2 H1 H2;
+    nnormalize in ⊢ (???%%);
+    napply (H1‡H2);
+##| #e H; nnormalize in ⊢ (???%%);
+    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))); ##[
+      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+      napply ((X‡#)‡#); ##]
+    napply #;
+##] nqed.
     
-    nchange in match (w2 ∈ 𝐋\p (?·?)) with (?∨?);
-    napply (.= 
-    
-
- //; napply (trans ?? ??? H E);
-   napply (trans (list S) (eq0 (LIST S)) ? [?] ?(*w1 [x] w2*) H E); 
-  nlapply (trans (list S) (eq0 (LIST S))).
-
-napply (.= H); nnormalize; nlapply (trans ? [x] w1 w2 E H); napply (.= ?) [napply (w1 = [x])] ##[##2: napply #; napply sym1; napply refl1 ]
+    FINQUI
 
 ndefinition epsilon ≝ 
   λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].