2 lift related bugs fixed!

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c8a19354cb74ad72f24a93403bb0ffab5cdb51f6..c4fc89f210b0c90f5a049d80442f0cf6b7222e11 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -71,7 +71,7 @@ nqed.
 include "hints_declaration.ma". 
 
 alias symbol "hint_decl" = "hint_decl_Type2".
-unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
+unification hint 0 ≔ A ⊢ carr1 (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A))) ≡ Ω^A.
 
 (************ SETS OVER SETOIDS ********************)
 
@@ -106,6 +106,10 @@ nqed.
 unification hint 0 ≔ A ⊢  
   carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
 
+(*CSC: non va!  
+unification hint 0 ≔ A ⊢  
+  carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*)
+
 nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @
   [ napply (λx,S. x ∈ S) 
@@ -116,10 +120,15 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid
   ##]
 nqed.
 
+(*CSC: bug qui se metto x o S al posto di ?
+nlemma foo: True.
+nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in
+    fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S);
+*)
 unification hint 0 ≔  A:setoid, x, S;  
          SS ≟ (pc ? S)
   (*-------------------------------------*) ⊢ 
-    fun21 ??? (mem_ok A) x S ≡ mem A SS x.
+    fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x.
 
 nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @
@@ -228,9 +237,31 @@ nlemma first_omomorphism_theorem_functions3:
  #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
 nqed.
 
-nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝
  { iso_f:> unary_morphism A B;
    f_closed: ∀x. x ∈ S → iso_f x ∈ T;
    f_sur: surjective … S T iso_f;
    f_inj: injective … S iso_f
  }.
+
+(*
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+ { iso_f:> unary_morphism A B;
+   f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}.
+   
+   
+ncheck (λA:?.
+   λB:?.
+    λS:?.
+     λT:?.
+      λxxx:isomorphism A B S T.
+       match xxx
+       return λxxx:isomorphism A B S T.
+               ∀x: carr A.
+                ∀x_72: mem (carr A) (pc A S) x.
+                 mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x)
+        with [ mk_isomorphism _ yyy ⇒ yyy ] ).   
+   
+   ;
+ }.
+*)