From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Jul 2010 15:46:33 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2870
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=31952b17e32c9e399d54485e031247250b1707a0;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 0b4c3365a..a495413f5 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -322,16 +322,18 @@ ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
 *; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
 nqed.
  
-nlemma d : ∀S:Alpha.
- ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
- ∀x,y:list S.x = y →
+nlemma d : ∀S:setoid1. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:S.x =_1 y → (Ex1 S (λw.ee x w)) =_1 (Ex1 S (λw.ee y w)).
  let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
   form x = form y.
  #S ee x y E;
  nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
  
  nnormalize;
- nlapply (exists_is_morph (list S) (list S) ? ?? E);
+  nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+
+ ncheck (exists_is_morph (LIST S) (LIST S) ? ?? (E‡#)).
+ nletin xxx ≝ (exists_is_morph); (LIST S)); (LIST S) ee x y E);
  
  nchange with (F x = F y);
  nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);