X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fexadecim_lemmas.ma;h=762ab5d03072b5c8695307e32f1d32ffe723da73;hb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;hp=19f9dc96073e61f82dd2b35f745df67f6d208b46;hpb=3e5c359c75874748cfed8a9046031b62396e0e6d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
index 19f9dc960..762ab5d03 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
@@ -382,23 +382,21 @@ nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 nqed.
 
 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
- #e1; #e2; #H;
- nletin K ≝ (bool_destruct ?? (e1 = e2) H);
- nelim e1 in K:(%) ⊢ %;
- nelim e2;
+ #e1; #e2;
+ ncases e1;
+ ncases e2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (bool_destruct ??? H)
  ##]
 nqed.
 
 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
- #e1; #e2; #H;
- nletin K ≝ (exadecim_destruct ?? (eq_ex e1 e2 = true) H);
- nelim e1 in K:(%) ⊢ %;
- nelim e2;
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (exadecim_destruct ??? H)
  ##]
 nqed.