-definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
-definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
-
-definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
-definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
-definition map2 ≝ add_maxcur_map map1 pluto.
-definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
-
-definition snap1 ≝ build_snapshot map2.
-
-definition map3 ≝ add_maxcur_map map2 pippo.
-definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
-definition map4 ≝ add_maxcur_map map3 pluto.
-definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
-
-definition snap2 ≝ build_snapshot map4.
-
-definition map5 ≝ add_maxcur_map map4 pippo.
-definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
-definition map6 ≝ add_maxcur_map map5 pluto.
-definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
-
-definition map7 ≝ rollback_map map6 snap2.
-
-definition map8 ≝ rollback_map map7 snap1.
-
-lemma checkenv : None ? = Some ? env6.
-normalize; elim daemon.
-qed.
-
-lemma checkmap : None ? = Some ? map8.
-normalize; elim daemon.
-qed.
-
-lemma checksnap : None ? = Some ? snap2.
-normalize; elim daemon.
-qed.
+definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
+definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
+
+definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
+definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
+definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
+definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
+definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
+definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
+
+definition env2' ≝ enter_env env2.
+definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
+
+definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
+definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
+definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
+definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
+definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
+definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
+
+definition env4' ≝ enter_env env4.
+definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
+
+definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
+definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
+definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
+definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
+definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
+definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
+
+definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
+
+definition map7 ≝ rollback_map env4 fenv4 fenv6 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
+
+definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
+
+definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.