...

[helm.git] / helm / software / matita / nlibrary / re / re-setoids.ma

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 0b4c3365a40932d43236debf28cd7c3634066bd4..a495413f5247ce283d82d3f4c085401b15af4fd3 100644 (file)
--- 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);