freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / universe / universe.ma

diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
index a673c999ba2f5147a25cc813c1ff21bee31405fb..061cccd3e99983d62b083210e9cc02890bfe54f0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -103,34 +103,8 @@ 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)).
-
-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.
-
 (* eqxx_to_eq universale *)
+(* serve l'assioma di equivalenza sulle dimostrazioni *)
 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,7 +112,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));
+ nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
+ #dim1;
+ napply (peqv_ind ? dim1 (λ_.?) ? dim2 (peqv_ax ? dim1 dim2));
  napply refl_eq.
 nqed.