Environment simplified.

diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
index 9f489b7924d7836d0e8d5b51916f27cd34adadc5..d8805d26991be6a98a9ba024e471a4e9587e7ccd 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -384,10 +384,10 @@ definition env_to_flatEnv_inv ≝
  λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
   ∀str.
    check_desc_env d e str →
-   (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧
+    check_env_map_align d e d map = true ∧ check_map_env_align d e map = true ∧
     check_id_map d map str ∧
     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
-    get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
+    get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
 
 lemma inv_to_checkdescflatenv :
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
@@ -527,10 +527,20 @@ let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_ty
   ].
 
 (* avanzamento dell'invariante *)
-axiom env_map_flatEnv_enter_aux : 
+lemma env_map_flatEnv_enter_aux : 
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
   env_to_flatEnv_inv d e map fe →
   env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+ unfold env_to_flatEnv_inv;
+ intros;
+ split; [ split [ split [ split | ] | ] | ]
+  [ elim daemon
+  | elim daemon;
+  | elim daemon;
+  | elim daemon;
+  | elim daemon;
+  ]
+qed.
 
 axiom env_map_flatEnv_add_aux : 
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.