+definition add_desc_env_flatEnv_fe ≝
+λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
+ fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
+ (DESC_ELEM c desc) ].
+
+let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
+ match trsf with
+ [ nil ⇒ (λx.x)
+ | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+ ].
+
+let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
+ Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
+ match trsf with
+ [ nil ⇒ (λx.x)
+ | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
+ (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
+ (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
+ ].
+
+(* ********************************************* *)
+
+(* fe <= fe' *)
+definition eq_flatEnv_elem ≝
+λe1,e2.match e1 with
+ [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
+ [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstrid a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
+let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
+match fe with
+ [ nil ⇒ true
+ | cons h tl ⇒ match fe' with
+ [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
+ ].
+
+lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ [ reflexivity
+ | simplify;
+ rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+ rewrite > H1;
+ reflexivity
+ ].
+qed.
+
+lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
+ intro;
+ elim fe 0;
+ [ intros; exists; [ apply fe' | reflexivity ]
+ | intros 4; elim fe';
+ [ simplify in H1:(%); destruct H1
+ | simplify in H2:(%);
+ rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
+ cases (H l1 (andb_true_true_r ?? H2));
+ simplify;
+ rewrite < H3;
+ exists; [ apply x | reflexivity ]
+ ]
+ ].
+qed.
+
+lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
+ intros;
+ elim fe;
+ [ simplify;
+ reflexivity
+ | simplify;
+ rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+ rewrite > H;
+ reflexivity
+ ].
+qed.
+
+lemma leflatenv_to_check :
+ ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (check_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatenv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro; simplify in H2:(%); elim H2;
+ | intros 3;
+ simplify;
+ cases (eqStrId_str str (get_name_flatVar a));
+ [ simplify; intro; apply H3
+ | simplify; apply H2
+ ]
+ ].
+qed.
+
+lemma leflatenv_to_get :
+ ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatenv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro;
+ simplify in H2:(%);
+ elim H2
+ | simplify;
+ intros 2;
+ cases (eqStrId_str str (get_name_flatVar a));
+ [ simplify;
+ intros;
+ reflexivity
+ | simplify;
+ unfold check_desc_flatEnv;
+ unfold get_desc_flatEnv;
+ cases (get_desc_flatEnv_aux l str);
+ [ simplify; intros; elim H3
+ | simplify; intros; rewrite < (H2 H3); reflexivity
+ ]
+ ]
+ ].
+qed.
+
+lemma leflatenv_trans :
+ ∀fe,fe',fe''.
+ le_flatEnv fe fe' = true →
+ le_flatEnv fe' fe'' = true →
+ le_flatEnv fe fe'' = true.
+ intros 4;
+ cases (leflatenv_to_le fe ? H);
+ rewrite < H1;
+ intro;
+ cases (leflatenv_to_le (fe@x) fe'' H2);
+ rewrite < H3;
+ rewrite > associative_append;
+ apply (le_to_leflatenv fe ?).
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_al :
+ ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
+ snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
+ a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
+ intro;
+ elim trsf;
+ [ simplify; reflexivity
+ | simplify;
+ elim a;
+ simplify;
+ rewrite > (H ????);
+ reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_l :
+ ∀trsf.∀d.∀m:aux_map_type d.∀l.
+ snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
+ l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
+ intros;
+ elim l;
+ [ simplify; reflexivity
+ | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
+ rewrite > H;
+ reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe :
+ ∀d.∀map:aux_map_type d.∀fe,trsf.
+ ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intros 3;
+ elim fe 0;
+ [ simplify;
+ intro;
+ exists;
+ [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+ | reflexivity
+ ]
+ | intros 4;
+ exists;
+ [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+ | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
+ rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
+ rewrite < (cons_append_commute ????);
+ reflexivity
+ ]
+ ].
+qed.
+
+lemma buildtrasfenvadd_to_le :
+ ∀d.∀m:aux_map_type d.∀fe,trsf.
+ le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
+ intros 4;
+ cases (env_map_flatEnv_add_aux_fe d m fe trsf);
+ rewrite < H;
+ rewrite > (le_to_leflatenv fe x);
+ reflexivity.
+qed.
+
+(* ********************************************* *)
+
+(* miscellanea *)
+lemma leave_env_enter_env : ∀d.∀e:aux_env_type d.leave_env d (enter_env d e) = e.
+ intros;
+ elim e;
+ reflexivity.
+qed.
+
+lemma leave_map_enter_map : ∀d.∀map. leave_map d (enter_map d map) = map.
+ intros;
+ elim map;
+ [ reflexivity
+ | simplify;
+ rewrite > H;
+ cases a;
+ simplify;
+ reflexivity
+ ]
+qed.
+
+lemma leave_add_enter_env_aux :
+ ∀d.∀a:aux_env_type d.∀trsf.∀c.
+ ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
+ intros 3;
+ elim trsf;
+ [ simplify; exists; [ apply c | reflexivity ]
+ | simplify; apply H
+ ].
+qed.
+
+lemma leave_add_enter_env :
+ ∀d.∀e:aux_env_type d.∀trsf.
+ leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
+ intros;
+ unfold enter_env;
+ lapply (leave_add_enter_env_aux d e trsf []);
+ cases Hletin;
+ rewrite > H;
+ simplify;
+ reflexivity.
+qed.
+
+(* ********************************************* *)
+
+(* invariante a un livello *)
+definition env_to_flatEnv_inv_one_level ≝
+ λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
+ ∀str.
+ check_desc_env d e str →
+ 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)).
+
+(* invariante su tutti i livelli *)
+let rec env_to_flatEnv_inv (d:nat) : aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop ≝
+ match d
+ return λd.aux_env_type d → aux_map_type d → aux_flatEnv_type → Prop
+ with
+ [ O ⇒ λe:aux_env_type O.λmap:aux_map_type O.λfe:aux_flatEnv_type.
+ env_to_flatEnv_inv_one_level O e map fe
+ | S n ⇒ λe:aux_env_type (S n).λmap:aux_map_type (S n).λfe:aux_flatEnv_type.
+ env_to_flatEnv_inv_one_level (S n) e map fe ∧
+ env_to_flatEnv_inv n (leave_env n e) (leave_map n map) fe