∀dimInv:env_to_flatEnv_inv d e m fe.
astfe_id fe b t.
intros 7;
- unfold env_to_flatEnv_inv;
elim a 0;
intros 3;
lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
- [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
- | rewrite > (proj2 ?? (H1 a1 H));
+ [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)))
+ | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H));
apply Hletin
].
qed.
∀dimLe:le_flatEnv fe fe' = true.
astfe_id fe' b t.
intros 8;
- unfold env_to_flatEnv_inv;
elim a 0;
intros 4;
lapply (ASTFE_ID fe' a1 ?);