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=061cccd3e99983d62b083210e9cc02890bfe54f0;hpb=34e2c8f59dd7924e15a7746644182d12ad09fed3;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 061cccd3e..21fd84675 100755
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -105,6 +105,13 @@ nqed.
 
 (* eqxx_to_eq universale *)
 (* serve l'assioma di equivalenza sulle dimostrazioni *)
+
+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;
+*)
+
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; nelim x;
  #u1; #dim1;
@@ -114,8 +121,7 @@ nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #H;
  nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
  #dim1;
- napply (peqv_ind ? dim1 (λ_.?) ? dim2 (peqv_ax ? dim1 dim2));
- napply refl_eq.
+ napply eqSUN_to_eq_aux.
 nqed.
 
 (* neq_to_neqxx universale *)