Many axioms are now proved... using many more (but simpler) axioms.

[helm.git] / helm / software / matita / contribs / assembly / compiler / ast_to_astfe.ma

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 5d7a6a622a8ee0626614cc2294d2d9e009576e99..90a59130a9e1064b1baaf6972ee175cd544892c9 100755 (executable)
--- 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 ?);