-(* bisogna dimostrare "defined_envList (S ...)"
- impossibile anche cercando di usare l'emulazione di inversion
-*)
-naxiom defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
+(* bisogna bypassare la carenza di inversion *)
+nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
+ #d; #l;
+ ngeneralize in match (refl_eq ? (S d));
+ (* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
+ ncases l in ⊢ (? ? % ? → %);
+ ##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
+ ##| ##2: #n; #dsc; #sub; #H;
+ nnormalize;
+ napply I
+ ##]
+nqed.