X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;h=6a5e204f332bf4f37b1801df9f313c525eaf2e5e;hb=34e2c8f59dd7924e15a7746644182d12ad09fed3;hp=73a2c8aa44d990cf42f80cc05e2c9946267cbea8;hpb=417792b30223b5edd4a9194193c7f34514bd0fa3;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index 73a2c8aa4..6a5e204f3 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -58,6 +58,8 @@ ndefinition defined_envList ≝
 (* 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.
+
 ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
 λd.λl:env_list (S d).
   match l
@@ -65,8 +67,4 @@ ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
   with
    [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
    | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
-   ] ?.
- napply (inv_envList ? l …);
- (* se apro l, a ritroso modifica il suo parametro destro d e non dimostro piu' nulla *)
- (* io pensavo di ottenere per env_nil l'assurdo S d = O ... *)
- ncases l;
+   ] (defined_envList_S d l).