From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 8 Sep 2010 21:51:05 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2836
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e1e5dc8f6e1299fe4368e38f252ae45c8a8a6c1;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index dcd9a226d..14d52373e 100644
--- 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 ⇒ { [ ] } | _ ⇒ ∅ ].