+ | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
+ λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+ match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
+ [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+ ([ tripleT ??? sName true sType ]@resTrsf)
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
+ ([ ASTFE_STM_INIT resFe true sType
+ (* l'id e' sull'ambiente arricchito *)
+ (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ true sType
+ (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
+ true sType
+ (newid_from_init sD sE sName true sType)
+ (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+ (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ resDimLe)
+ (* l'init e' sull'ambiente non arricchito *)
+ (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
+ sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+ resMap resFe
+ (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+ (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
+ ]@resLStm) ]
+
+ | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒