-lemma env_map_flatEnv_add_aux_fe_al :
- ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
- snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
- a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
- intro;
- elim trsf;
- [ simplify; reflexivity
- | simplify;
- elim a;
- simplify;
- rewrite > (H ????);
- reflexivity
- ].
-qed.
-
-lemma env_map_flatEnv_add_aux_fe_l :
- ∀trsf.∀d.∀m:aux_map_type d.∀l.
- snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
- l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
- intros;
- elim l;
- [ simplify; reflexivity
- | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
- rewrite > H;
- reflexivity
- ].
-qed.
-
-lemma env_map_flatEnv_add_aux_fe :
- ∀d.∀map:aux_map_type d.∀fe,trsf.
- ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
- intros 3;
- elim fe 0;
- [ simplify;
- intro;
- exists;
- [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
- | reflexivity
- ]
- | intros 4;
- exists;
- [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
- | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
- rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
- rewrite < (cons_append_commute ????);
- reflexivity
- ]
- ].
-qed.
-
-lemma buildtrasfenvadd_to_le :
- ∀d.∀m:aux_map_type d.∀fe,trsf.
- le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
- intros 4;
- cases (env_map_flatEnv_add_aux_fe d m fe trsf);
- rewrite < H;
- rewrite > (le_to_leflatenv fe x);
- reflexivity.
-qed.
-
-axiom env_map_flatEnv_leave_aux :
- ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
- env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
- env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
-
-lemma leave_add_enter_env_aux :
- ∀d.∀a:aux_env_type d.∀trsf.∀c.
- ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
- intros 3;
- elim trsf;
- [ simplify; exists; [ apply c | reflexivity ]
- | simplify; apply H
- ].
-qed.
-
-lemma leave_add_enter_env :
- ∀d.∀e:aux_env_type d.∀trsf.
- leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
- intros;
- unfold enter_env;
- lapply (leave_add_enter_env_aux d e trsf []);
- cases Hletin;
- rewrite > H;
- simplify;
- reflexivity.
-qed.