-(* leave: elimina la testa (il "cur" corrente) *)
-let rec leave_map d (map:aux_map_type (S d)) on map ≝
- match map with
- [ nil ⇒ []
- | cons h t ⇒
- (MAP_ELEM d
- (get_name_mapElem (S d) h)
- (get_max_mapElem (S d) h)
- (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
- )::(leave_map d t)
- ].
+lemma checkdescenter_to_checkdesc :
+ ∀d.∀e:aux_env_type d.∀str.
+ check_desc_env (S d) (enter_env d e) str →
+ check_desc_env d e str.
+ intros;
+ unfold enter_env in H:(%);
+ simplify in H:(%);
+ apply H.
+qed.
+
+lemma checkenvmapalign_to_enter :
+ ∀de.∀e:aux_env_type de.∀dm.∀m:aux_map_type dm.
+ check_env_map_align de e dm m =
+ check_env_map_align (S de) (enter_env de e) (S dm) (enter_map dm m).
+ intros 4;
+ unfold enter_env;
+ simplify;
+ elim e 0;
+ [ simplify;
+ intro;
+ elim l 0;
+ [ simplify;
+ reflexivity
+ | simplify;
+ intros;
+ rewrite > (getidmap_to_enter ???);
+ rewrite < H;
+ cases (get_id_map_aux dm m (get_name_var a));
+ [ simplify;
+ reflexivity
+ | simplify;
+ rewrite > H;
+ reflexivity
+ ]
+ ]
+ | simplify;
+ intros 2;
+ elim l 0;
+ [ simplify;
+ intros;
+ apply H
+ | intros;
+ simplify;
+ rewrite > (getidmap_to_enter ???);
+ cases (get_id_map_aux dm m (get_name_var a));
+ [ simplify;
+ reflexivity
+ | simplify;
+ apply (H e1 H1)
+ ]
+ ]
+ ].
+qed.
+
+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;
+ [ rewrite < (checkenvmapalign_to_enter ???);
+ apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
+ | (* TO DO !!! *) elim daemon
+ ]
+ | unfold check_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+ ]
+ | unfold get_id_map;
+ rewrite > (getidmap_to_enter ???);
+ apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
+ ].
+qed.