-(* 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)).