(* 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;
#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 *)