From 31952b17e32c9e399d54485e031247250b1707a0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Jul 2010 15:46:33 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/re/re-setoids.ma | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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); -- 2.39.2