freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / environment.ma

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index 73a2c8aa44d990cf42f80cc05e2c9946267cbea8..6a5e204f332bf4f37b1801df9f313c525eaf2e5e 100755 (executable)
--- 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).