X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Funiverse%2Funiverse.ma;h=0db667a0f375b7c1a450ed7d9cc9b14d3682a424;hb=d97886196d2c730f72312b226bebc388be08f39e;hp=21fd84675aebe79b938ef65f7c07a63a034303d3;hpb=c6ec0dc44c2e592c7b1323304052bc1a523e7c22;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 21fd84675..0db667a0f 100755
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -104,24 +104,13 @@ nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
 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;
-*)
+(* !!! evidente ma come si fa? *)
+naxiom eqSUN_to_eq_aux : ∀l,x,y.((getelem l x) = (getelem l y)) → x = y.
 
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
- #l; #x; nelim x;
- #u1; #dim1;
- #y; nelim y;
- #u2; #dim2;
- nchange with ((eq_nat u1 u2 = true) → ?);
- #H;
- nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
- #dim1;
- napply eqSUN_to_eq_aux.
+ #l; #x; #y;
+ nchange with ((eq_nat (getelem ? x) (getelem ? y) = true) → x = y);
+ #H; napply (eqSUN_to_eq_aux l x y (eqnat_to_eq … H)).
 nqed.
 
 (* neq_to_neqxx universale *)
@@ -200,13 +189,13 @@ nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
 
 (* esempio0: universo ottale *)
 ndefinition oct0 ≝ O.
-ndefinition oct1 ≝ S O.
-ndefinition oct2 ≝ S (S O).
-ndefinition oct3 ≝ S (S (S O)).
-ndefinition oct4 ≝ S (S (S (S O))).
-ndefinition oct5 ≝ S (S (S (S (S O)))).
-ndefinition oct6 ≝ S (S (S (S (S (S O))))).
-ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
+ndefinition oct1 ≝ nat1.
+ndefinition oct2 ≝ nat2.
+ndefinition oct3 ≝ nat3.
+ndefinition oct4 ≝ nat4.
+ndefinition oct5 ≝ nat5.
+ndefinition oct6 ≝ nat6.
+ndefinition oct7 ≝ nat7.
 
 ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».