+definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+ match l
+ return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
+ with
+ [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+ | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t
+ ] p in value.
+
+definition get_first_mapList : Πd.map_list d → ? → option nat ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+ match l
+ return λX.λY:map_list X.defined_mapList X Y → option nat
+ with
+ [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+ | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h
+ ] p in value.
+
+inductive map_elem (d:nat) : Type ≝
+MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
+
+definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
+definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
+definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
+
+definition aux_map_type ≝ λd.list (map_elem d).
+
+definition empty_map ≝ nil (map_elem O).
+
+lemma defined_mapList_S_to_true :
+∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
+ intros;
+ inversion l;
+ [ intros; destruct H
+ | intros; simplify; reflexivity
+ ]
+qed.
+
+lemma defined_mapList_get :
+ ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
+ intros 2;
+ rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
+ apply I.
+qed.
+
+(* get_id *)
+let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
+ match map with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)
+ | false ⇒ get_id_map_aux d t name
+ ]
+ ].
+
+definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* get_max *)
+let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
+ match map with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+ [ true ⇒ Some ? (get_max_mapElem d h)
+ | false ⇒ get_max_map_aux d t name
+ ]
+ ].
+
+definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* check_id *)
+definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbidmap_to_checkidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+ checkb_id_map d map name = true → check_id_map d map name.
+ unfold checkb_id_map;
+ unfold check_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; destruct H
+ | simplify; intros; apply I
+ ].
+qed.
+
+definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbidmap_to_checknotidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+ checknotb_id_map d map name = true → checknot_id_map d map name.
+ unfold checknotb_id_map;
+ unfold checknot_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; apply I
+ | simplify; intros; destruct H
+ ].
+qed.
+
+(* get_desc *)
+let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
+ match fe with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
+ [ true ⇒ Some ? (get_desc_flatVar h)
+ | false ⇒ get_desc_flatEnv_aux t name
+ ]
+ ].
+
+definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with