+axiom get_desc_env_aux_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env_aux d (build_trasfEnv_env d trsf e) str =
+ get_desc_env_aux d e str.
+
+lemma get_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_env d e str.
+ intros;
+ unfold get_desc_env;
+ rewrite > (get_desc_env_aux_not_occurs ???? H);
+ reflexivity.
+qed.
+
+lemma check_desc_env_not_occurs :
+ ∀d.∀e:aux_env_type d.∀trsf.∀str.
+ occurs_in_trsf trsf str = false →
+ check_desc_env d (build_trasfEnv_env d trsf e) str →
+ check_desc_env d e str.
+ intros 5;
+ unfold check_desc_env;
+ intro;
+ rewrite < (get_desc_env_aux_not_occurs ???? H);
+ apply H1.
+qed.
+
+axiom get_id_map_aux_add_occurs :
+ ∀d.∀map:aux_map_type d.∀fe,trsf,str.
+ occurs_in_trsf trsf str = true →
+ ∃x.get_id_map_aux d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str = Some ? x.
+
+lemma check_id_map_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str.
+ intros;
+ cases (get_id_map_aux_add_occurs d map fe trsf str H);
+ unfold check_id_map;
+ rewrite > H1;
+ simplify;
+ apply I.
+qed.
+
+axiom check_desc_flatEnv_occurs :
+ ∀d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ check_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom get_desc_env_eq_get_desc_flatEnv_occurs :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.∀str.
+ occurs_in_trsf trsf str = true →
+ get_desc_env d (build_trasfEnv_env d trsf e) str =
+ get_desc_flatEnv (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+ (STR_ID str (get_id_map d (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) str)).
+
+axiom leave_env_build_trasfEnv :
+ ∀d.∀e:aux_env_type (S d).∀trsf.
+ leave_env d (build_trasfEnv_env (S d) trsf e) = leave_env d e.
+
+axiom leave_map_build_trasfEnv_mapFe:
+ ∀d.∀map:aux_map_type (S d).∀fe.∀trsf.
+ leave_map d (fst ?? (build_trasfEnv_mapFe (S d) trsf (pair ?? map fe))) =
+ leave_map d map.
+
+lemma env_map_flatEnv_add_aux :