X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Funiverse%2Funiverse.ma;h=21fd84675aebe79b938ef65f7c07a63a034303d3;hb=8134330933e377a344b5ee38890198dc0b653428;hp=a673c999ba2f5147a25cc813c1ff21bee31405fb;hpb=a62de71cf6821c955bd41fa691c52ea62173f25d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
index a673c999b..21fd84675 100755
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -103,34 +103,15 @@ nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
  ##]
 nqed.
 
-(* perche' non si riesce a dimstrare ??? *
-nlemma SUN_construct
- : ∀l.∀u.
-   ∀dim1,dim2:(member_natList u l = true).
-   ((S_EL l u dim1) = (S_EL l u dim2)).
- #l; #u; #dim1; #dim2;
- nchange with (S_EL l u dim1 = S_EL l u dim1);
- napply refl_eq.
-nqed.
-*)
-naxiom SUN_construct
- : ∀l.∀u.
-   ∀dim1,dim2:(member_natList u l = true).
-   ((S_EL l u dim1) = (S_EL l u dim2)).
+(* eqxx_to_eq universale *)
+(* serve l'assioma di equivalenza sulle dimostrazioni *)
 
-nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
- #l; #x; nelim x;
- #u1; #dim1;
- #y; nelim y;
- #u2; #dim2;
- nchange with (u1 = u2 → ?);
- #H;
- nrewrite > H in dim1:(%) ⊢ %;
- #dim1;
- napply (SUN_construct l u2 dim1 dim2).
-nqed.
+naxiom eqSUN_to_eq_aux : ∀l,e.∀dim1,dim2:((member_natList e l) = true).S_EL l e dim1 = S_EL l e dim2.
+(* mi dice matita/logic/equality/eq.ind not found che e' vero perche' uso il mio...
+ #l; #e; #dim1; #dim2;
+ nauto library;
+*)
 
-(* eqxx_to_eq universale *)
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; nelim x;
  #u1; #dim1;
@@ -138,8 +119,9 @@ nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #u2; #dim2;
  nchange with ((eq_nat u1 u2 = true) → ?);
  #H;
- nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
- napply refl_eq.
+ nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
+ #dim1;
+ napply eqSUN_to_eq_aux.
 nqed.
 
 (* neq_to_neqxx universale *)