+(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
+let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
+match e with
+ [ nil ⇒ None ?
+ | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_flatEnv_aux tl str ]].
+
+definition get_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with
+ [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+ unfold checkb_desc_flatEnv;
+ unfold check_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux e str);
+ elim K;
+ [ normalize; autobatch |
+ normalize; autobatch ]
+qed.
+
+(* aggiungi descrittore ad ambiente: in coda *)
+definition add_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
+ e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
+
+(* controllo 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 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 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_nameId_flatVar a));
+ [ simplify; intro; apply H3
+ | simplify;
+ apply H2
+ ]
+ ].
+qed.
+
+lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
+intros;
+ change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
+ elim fe 0;
+ [ 1: reflexivity
+ | 2: do 3 intro;
+ unfold le_flatEnv;
+ change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ unfold eq_flatEnv_elem;
+ elim a;
+ change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+ rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ rewrite > H;
+ reflexivity
+ ].
+qed.
+