freescale translation (work in progress)

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / exadecim_lemmas.ma

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 19f9dc96073e61f82dd2b35f745df67f6d208b46..762ab5d03072b5c8695307e32f1d32ffe723da73 100755 (executable)
--- 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.