X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_to_astfe.ma;h=90a59130a9e1064b1baaf6972ee175cd544892c9;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=5d7a6a622a8ee0626614cc2294d2d9e009576e99;hpb=be527f5bd4acaf530d8843b23e6849fd5211e1fc;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
index 5d7a6a622..90a59130a 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -36,12 +36,11 @@ lemma ast_to_astfe_id :
  ∀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.
@@ -53,7 +52,6 @@ lemma ast_to_astfe_retype_id :
  ∀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 ?);