∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
env_to_flatEnv_inv d e map fe →
env_to_flatEnv_inv d
(build_trasfEnv_env d trsf e)
(fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
env_to_flatEnv_inv d e map fe →
env_to_flatEnv_inv d
(build_trasfEnv_env d trsf e)
(fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).