freescale porting, work in progress

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 7dd405eebcde214f4c503e128f0bfe88553126f1..86e6629dc9db8395d2d5b36521064b821dc8a9f6 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -369,7 +369,9 @@ ndefinition w16_to_recw16_aux3 ≝
  ].
 
 nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
- #n; #e; nelim e; #input; napply (w16_S ? input).
+ #n; #e; nelim e;
+ (* napply (exadecim_ind … e); funziona *)
+ #input; napply (w16_S ? input).
 nqed.
 
 nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉.