X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftranslation.ma;h=0996948942bad7c8c8cd7b4809456eaa72acc96b;hb=a62de71cf6821c955bd41fa691c52ea62173f25d;hp=661737793505a9660d138755d3ea7311128c3f9f;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 661737793..099694894 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -76,13 +76,11 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
- #m; #b1; #b2; #H;
- nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+  [ TByte b1 ⇒ match tb2 with
+   [ TByte b2 ⇒ eq_b8 b1 b2 ]].
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 ninductive MA_check : instr_mode → Type ≝