From 5683cf231fa2ac8abade3b70aea1af995cc04379 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Thu, 21 Jan 2010 19:39:17 +0000
Subject: [PATCH]

---
 .../contribs/ng_assembly/common/ascii.ma      |   2 +-
 .../ng_assembly/common/ascii_lemmas.ma        | 130 +++++++++---------
 .../contribs/ng_assembly/common/list.ma       |   2 +-
 .../ng_assembly/common/list_lemmas.ma         |   6 +-
 .../ng_assembly/common/list_utility.ma        |  22 +--
 .../ng_assembly/common/list_utility_lemmas.ma | 103 +++++++++-----
 .../matita/contribs/ng_assembly/common/nat.ma |   2 +-
 .../contribs/ng_assembly/common/nat_lemmas.ma |  12 +-
 .../contribs/ng_assembly/common/nat_to_num.ma |   2 +-
 .../contribs/ng_assembly/common/option.ma     |   2 +-
 .../ng_assembly/common/option_lemmas.ma       |  36 +++--
 .../contribs/ng_assembly/common/prod.ma       |  32 +++--
 .../ng_assembly/common/prod_lemmas.ma         |  22 +--
 .../contribs/ng_assembly/common/sigma.ma      |  10 +-
 .../contribs/ng_assembly/common/string.ma     |   2 +-
 .../ng_assembly/common/string_lemmas.ma       |   2 +-
 .../contribs/ng_assembly/common/theory.ma     | 109 ++++++++++++---
 .../matita/contribs/ng_assembly/depends       |   2 +-
 .../contribs/ng_assembly/num/bitrigesim.ma    |   2 +-
 .../ng_assembly/num/bitrigesim_lemmas.ma      |  68 ++++-----
 .../matita/contribs/ng_assembly/num/bool.ma   |   2 +-
 .../contribs/ng_assembly/num/bool_lemmas.ma   |  40 +++---
 .../matita/contribs/ng_assembly/num/byte8.ma  |   2 +-
 .../contribs/ng_assembly/num/byte8_lemmas.ma  |   2 +-
 .../contribs/ng_assembly/num/exadecim.ma      |   2 +-
 .../ng_assembly/num/exadecim_lemmas.ma        |   6 +-
 .../matita/contribs/ng_assembly/num/oct.ma    |   2 +-
 .../contribs/ng_assembly/num/oct_lemmas.ma    |   6 +-
 .../contribs/ng_assembly/num/quatern.ma       |   2 +-
 .../ng_assembly/num/quatern_lemmas.ma         |   6 +-
 .../matita/contribs/ng_assembly/num/word16.ma |   2 +-
 .../contribs/ng_assembly/num/word16_lemmas.ma |   2 +-
 .../matita/contribs/ng_assembly/num/word32.ma |   2 +-
 .../contribs/ng_assembly/num/word32_lemmas.ma |   2 +-
 34 files changed, 396 insertions(+), 250 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii.ma b/helm/software/matita/contribs/ng_assembly/common/ascii.ma
index e5e195286..ddb65df3a 100755
--- a/helm/software/matita/contribs/ng_assembly/common/ascii.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas.ma
index 0d10de49d..dd1eec486 100755
--- a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* DEFINIZIONE ASCII MINIMALE *)
 (* ************************** *)
 
+(*
 ndefinition ascii_destruct_aux ≝
 Πc1,c2.ΠP:Prop.c1 = c2 →
  match eq_ascii c1 c2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ nlemma ascii_destruct : ascii_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma eq_to_eqascii : ∀n1,n2.n1 = n2 → eq_ascii n1 n2 = true.
  #n1; #n2; #H;
@@ -55,69 +57,69 @@ nlemma neqascii_to_neq : ∀n1,n2.eq_ascii n1 n2 = false → n1 ≠ n2.
  ##]
 nqed.
 
-nlemma eqascii_to_eq1 : ∀a2.eq_ascii ch_0 a2 = true → ch_0 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq2 : ∀a2.eq_ascii ch_1 a2 = true → ch_1 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq3 : ∀a2.eq_ascii ch_2 a2 = true → ch_2 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq4 : ∀a2.eq_ascii ch_3 a2 = true → ch_3 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq5 : ∀a2.eq_ascii ch_4 a2 = true → ch_4 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq6 : ∀a2.eq_ascii ch_5 a2 = true → ch_5 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq7 : ∀a2.eq_ascii ch_6 a2 = true → ch_6 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq8 : ∀a2.eq_ascii ch_7 a2 = true → ch_7 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq9 : ∀a2.eq_ascii ch_8 a2 = true → ch_8 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq10 : ∀a2.eq_ascii ch_9 a2 = true → ch_9 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq11 : ∀a2.eq_ascii ch__ a2 = true → ch__ = a2. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq12 : ∀a2.eq_ascii ch_A a2 = true → ch_A = a2. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq13 : ∀a2.eq_ascii ch_B a2 = true → ch_B = a2. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq14 : ∀a2.eq_ascii ch_C a2 = true → ch_C = a2. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq15 : ∀a2.eq_ascii ch_D a2 = true → ch_D = a2. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq16 : ∀a2.eq_ascii ch_E a2 = true → ch_E = a2. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq17 : ∀a2.eq_ascii ch_F a2 = true → ch_F = a2. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq18 : ∀a2.eq_ascii ch_G a2 = true → ch_G = a2. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq19 : ∀a2.eq_ascii ch_H a2 = true → ch_H = a2. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq20 : ∀a2.eq_ascii ch_I a2 = true → ch_I = a2. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq21 : ∀a2.eq_ascii ch_J a2 = true → ch_J = a2. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq22 : ∀a2.eq_ascii ch_K a2 = true → ch_K = a2. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq23 : ∀a2.eq_ascii ch_L a2 = true → ch_L = a2. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq24 : ∀a2.eq_ascii ch_M a2 = true → ch_M = a2. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq25 : ∀a2.eq_ascii ch_N a2 = true → ch_N = a2. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq26 : ∀a2.eq_ascii ch_O a2 = true → ch_O = a2. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq27 : ∀a2.eq_ascii ch_P a2 = true → ch_P = a2. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq28 : ∀a2.eq_ascii ch_Q a2 = true → ch_Q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq29 : ∀a2.eq_ascii ch_R a2 = true → ch_R = a2. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq30 : ∀a2.eq_ascii ch_S a2 = true → ch_S = a2. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq31 : ∀a2.eq_ascii ch_T a2 = true → ch_T = a2. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq32 : ∀a2.eq_ascii ch_U a2 = true → ch_U = a2. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq33 : ∀a2.eq_ascii ch_V a2 = true → ch_V = a2. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq34 : ∀a2.eq_ascii ch_W a2 = true → ch_W = a2. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq35 : ∀a2.eq_ascii ch_X a2 = true → ch_X = a2. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq36 : ∀a2.eq_ascii ch_Y a2 = true → ch_Y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq37 : ∀a2.eq_ascii ch_Z a2 = true → ch_Z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq38 : ∀a2.eq_ascii ch_a a2 = true → ch_a = a2. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq39 : ∀a2.eq_ascii ch_b a2 = true → ch_b = a2. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq40 : ∀a2.eq_ascii ch_c a2 = true → ch_c = a2. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq41 : ∀a2.eq_ascii ch_d a2 = true → ch_d = a2. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq42 : ∀a2.eq_ascii ch_e a2 = true → ch_e = a2. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq43 : ∀a2.eq_ascii ch_f a2 = true → ch_f = a2. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq44 : ∀a2.eq_ascii ch_g a2 = true → ch_g = a2. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq45 : ∀a2.eq_ascii ch_h a2 = true → ch_h = a2. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq46 : ∀a2.eq_ascii ch_i a2 = true → ch_i = a2. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq47 : ∀a2.eq_ascii ch_j a2 = true → ch_j = a2. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq48 : ∀a2.eq_ascii ch_k a2 = true → ch_k = a2. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq49 : ∀a2.eq_ascii ch_l a2 = true → ch_l = a2. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq50 : ∀a2.eq_ascii ch_m a2 = true → ch_m = a2. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq51 : ∀a2.eq_ascii ch_n a2 = true → ch_n = a2. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq52 : ∀a2.eq_ascii ch_o a2 = true → ch_o = a2. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq53 : ∀a2.eq_ascii ch_p a2 = true → ch_p = a2. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq54 : ∀a2.eq_ascii ch_q a2 = true → ch_q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq55 : ∀a2.eq_ascii ch_r a2 = true → ch_r = a2. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq56 : ∀a2.eq_ascii ch_s a2 = true → ch_s = a2. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq57 : ∀a2.eq_ascii ch_t a2 = true → ch_t = a2. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq58 : ∀a2.eq_ascii ch_u a2 = true → ch_u = a2. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq59 : ∀a2.eq_ascii ch_v a2 = true → ch_v = a2. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq60 : ∀a2.eq_ascii ch_w a2 = true → ch_w = a2. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq61 : ∀a2.eq_ascii ch_x a2 = true → ch_x = a2. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq62 : ∀a2.eq_ascii ch_y a2 = true → ch_y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqascii_to_eq63 : ∀a2.eq_ascii ch_z a2 = true → ch_z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
+nlemma eqascii_to_eq1 : ∀a2.eq_ascii ch_0 a2 = true → ch_0 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq2 : ∀a2.eq_ascii ch_1 a2 = true → ch_1 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq3 : ∀a2.eq_ascii ch_2 a2 = true → ch_2 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq4 : ∀a2.eq_ascii ch_3 a2 = true → ch_3 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq5 : ∀a2.eq_ascii ch_4 a2 = true → ch_4 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq6 : ∀a2.eq_ascii ch_5 a2 = true → ch_5 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq7 : ∀a2.eq_ascii ch_6 a2 = true → ch_6 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq8 : ∀a2.eq_ascii ch_7 a2 = true → ch_7 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq9 : ∀a2.eq_ascii ch_8 a2 = true → ch_8 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq10 : ∀a2.eq_ascii ch_9 a2 = true → ch_9 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq11 : ∀a2.eq_ascii ch__ a2 = true → ch__ = a2. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq12 : ∀a2.eq_ascii ch_A a2 = true → ch_A = a2. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq13 : ∀a2.eq_ascii ch_B a2 = true → ch_B = a2. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq14 : ∀a2.eq_ascii ch_C a2 = true → ch_C = a2. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq15 : ∀a2.eq_ascii ch_D a2 = true → ch_D = a2. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq16 : ∀a2.eq_ascii ch_E a2 = true → ch_E = a2. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq17 : ∀a2.eq_ascii ch_F a2 = true → ch_F = a2. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq18 : ∀a2.eq_ascii ch_G a2 = true → ch_G = a2. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq19 : ∀a2.eq_ascii ch_H a2 = true → ch_H = a2. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq20 : ∀a2.eq_ascii ch_I a2 = true → ch_I = a2. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq21 : ∀a2.eq_ascii ch_J a2 = true → ch_J = a2. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq22 : ∀a2.eq_ascii ch_K a2 = true → ch_K = a2. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq23 : ∀a2.eq_ascii ch_L a2 = true → ch_L = a2. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq24 : ∀a2.eq_ascii ch_M a2 = true → ch_M = a2. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq25 : ∀a2.eq_ascii ch_N a2 = true → ch_N = a2. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq26 : ∀a2.eq_ascii ch_O a2 = true → ch_O = a2. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq27 : ∀a2.eq_ascii ch_P a2 = true → ch_P = a2. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq28 : ∀a2.eq_ascii ch_Q a2 = true → ch_Q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq29 : ∀a2.eq_ascii ch_R a2 = true → ch_R = a2. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq30 : ∀a2.eq_ascii ch_S a2 = true → ch_S = a2. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq31 : ∀a2.eq_ascii ch_T a2 = true → ch_T = a2. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq32 : ∀a2.eq_ascii ch_U a2 = true → ch_U = a2. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq33 : ∀a2.eq_ascii ch_V a2 = true → ch_V = a2. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq34 : ∀a2.eq_ascii ch_W a2 = true → ch_W = a2. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq35 : ∀a2.eq_ascii ch_X a2 = true → ch_X = a2. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq36 : ∀a2.eq_ascii ch_Y a2 = true → ch_Y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq37 : ∀a2.eq_ascii ch_Z a2 = true → ch_Z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq38 : ∀a2.eq_ascii ch_a a2 = true → ch_a = a2. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq39 : ∀a2.eq_ascii ch_b a2 = true → ch_b = a2. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq40 : ∀a2.eq_ascii ch_c a2 = true → ch_c = a2. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq41 : ∀a2.eq_ascii ch_d a2 = true → ch_d = a2. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq42 : ∀a2.eq_ascii ch_e a2 = true → ch_e = a2. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq43 : ∀a2.eq_ascii ch_f a2 = true → ch_f = a2. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq44 : ∀a2.eq_ascii ch_g a2 = true → ch_g = a2. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq45 : ∀a2.eq_ascii ch_h a2 = true → ch_h = a2. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq46 : ∀a2.eq_ascii ch_i a2 = true → ch_i = a2. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq47 : ∀a2.eq_ascii ch_j a2 = true → ch_j = a2. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq48 : ∀a2.eq_ascii ch_k a2 = true → ch_k = a2. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq49 : ∀a2.eq_ascii ch_l a2 = true → ch_l = a2. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq50 : ∀a2.eq_ascii ch_m a2 = true → ch_m = a2. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq51 : ∀a2.eq_ascii ch_n a2 = true → ch_n = a2. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq52 : ∀a2.eq_ascii ch_o a2 = true → ch_o = a2. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq53 : ∀a2.eq_ascii ch_p a2 = true → ch_p = a2. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq54 : ∀a2.eq_ascii ch_q a2 = true → ch_q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq55 : ∀a2.eq_ascii ch_r a2 = true → ch_r = a2. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq56 : ∀a2.eq_ascii ch_s a2 = true → ch_s = a2. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq57 : ∀a2.eq_ascii ch_t a2 = true → ch_t = a2. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq58 : ∀a2.eq_ascii ch_u a2 = true → ch_u = a2. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq59 : ∀a2.eq_ascii ch_v a2 = true → ch_v = a2. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq60 : ∀a2.eq_ascii ch_w a2 = true → ch_w = a2. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq61 : ∀a2.eq_ascii ch_x a2 = true → ch_x = a2. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq62 : ∀a2.eq_ascii ch_y a2 = true → ch_y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqascii_to_eq63 : ∀a2.eq_ascii ch_z a2 = true → ch_z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
 
 nlemma eqascii_to_eq : ∀c1,c2.eq_ascii c1 c2 = true → c1 = c2.
  #c1; ncases c1;
diff --git a/helm/software/matita/contribs/ng_assembly/common/list.ma b/helm/software/matita/contribs/ng_assembly/common/list.ma
index d4571fa92..5bd83a936 100644
--- a/helm/software/matita/contribs/ng_assembly/common/list.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
index 90461cfca..3be3a0a89 100644
--- a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -42,6 +42,7 @@ nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
  #T; #x; #y; #H;
  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
@@ -50,6 +51,7 @@ nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → F
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
  #T; #x; #y; #H;
  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
@@ -121,6 +123,7 @@ nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
  #T; #x1; #x2; #y1; #H;
  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
@@ -129,6 +132,7 @@ nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  #T; #x1; #x2; #y2; #H;
  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index 1c062a912..154d85d36 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -95,7 +95,7 @@ nlemma fold_right_list2_aux1 :
  #T; #h; #t;
  nnormalize;
  #H;
- napply (nat_destruct_0_S ? H).
+ ndestruct (*napply (nat_destruct_0_S ? H)*).
 nqed.
 
 nlemma fold_right_list2_aux2 :
@@ -103,7 +103,7 @@ nlemma fold_right_list2_aux2 :
  #T; #h; #t;
  nnormalize;
  #H;
- napply (nat_destruct_S_0 ? H).
+ ndestruct (*napply (nat_destruct_S_0 ? H)*).
 nqed.
 
 nlemma fold_right_list2_aux3 :
@@ -114,10 +114,10 @@ nlemma fold_right_list2_aux3 :
  ##[ ##1: nnormalize; #H; napply refl_eq
  ##| ##2: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
-          nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
+          ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
  ##| ##3: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
-          nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
+          ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
           nchange with ((S (len_list T l1)) = (S (len_list T l)));
@@ -162,7 +162,7 @@ nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
 
 (* abs elem *)
 ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
- #T; nnormalize; #n; #H; napply (bool_destruct … H). nqed.
+ #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
 
 ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
@@ -241,8 +241,8 @@ nlemma fold_right_neList2_aux1 :
  nnormalize;
  ncases t';
  nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
  ##]
 nqed.
 
@@ -252,8 +252,8 @@ nlemma fold_right_neList2_aux2 :
  nnormalize;
  ncases t;
  nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
  ##]
 nqed.
 
@@ -316,7 +316,7 @@ nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 
 (* abs elem *)
 ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
- #T; #h; #n; nnormalize; #H; napply (bool_destruct … H). nqed.
+ #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
 
 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
index da7c6158e..971b10604 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -32,7 +32,7 @@ nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 
  nelim l1;
  ##[ ##1: #l2; ncases l2; nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
+          ##| ##2: #h; #t; #H; ndestruct (*nelim (nat_destruct_0_S ? H)*)
           ##]
  ##| ##2: #h; #l2; ncases l2; nnormalize;
           ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
@@ -52,11 +52,11 @@ nlemma symmetric_foldrightlist2_aux
           ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
           ##| ##2: #h; #l; #H1; #H2; #H3;
                    nchange in H1:(%) with (O = (S (len_list ? l)));
-                   nelim (nat_destruct_0_S ? H1)
+                   ndestruct (*nelim (nat_destruct_0_S ? H1)*)
           ##]
  ##| ##2: #h3; #l3; #H; #l2; ncases l2;
           ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
-                   nelim (nat_destruct_S_0 ? H1)
+                   ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
           ##| ##2: #h4; #l4; #H1; #H2; #H3;
                    nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
                    nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
@@ -106,10 +106,12 @@ nlemma bfoldrightlist2_to_eq
  nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: #H; #H1; napply refl_eq
-          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##[ ##1: #H1; nnormalize; #H2;
+                   ndestruct (*napply (bool_destruct … H2)*)
           ##| ##2: #hh2; #ll2; #H1; #H2;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
@@ -127,10 +129,14 @@ nlemma eq_to_bfoldrightlist2
  nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: #H; #H1; nnormalize; napply refl_eq
-          ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
+          ##| ##2: #hh2; #ll2; #H; #H1;
+                   (* !!! ndestruct: assert false *)
+                   nelim (list_destruct_nil_cons ??? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
+          ##[ ##1: #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   nelim (list_destruct_cons_nil ??? H2)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
                    nrewrite > (list_destruct_1 … H2);
                    nrewrite > (H1 hh2 hh2 (refl_eq …));
@@ -147,10 +153,12 @@ nlemma bfoldrightlist2_to_lenlist
  nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: nnormalize; #H; napply refl_eq
-          ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
+          ##| ##2: nnormalize; #hh; #tt; #H;
+                   ndestruct (*napply (bool_destruct … H)*)
           ##]
  ##| ##2: #hh; #tt; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
+          ##[ ##1: nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
           ##| ##2: #hh1; #tt1; #H1; nnormalize;
                    nrewrite > (H tt1 ?);
                    ##[ ##1: napply refl_eq
@@ -166,11 +174,15 @@ nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.deci
  ##[ ##1: #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1; napply (list_destruct_nil_cons T … H1)
+                   nnormalize; #H1;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H1)
           ##]
  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2; napply (list_destruct_cons_nil T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H2)
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
@@ -192,11 +204,16 @@ nlemma nbfoldrightlist2_to_neq
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
-          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+          ##[ ##1: #H; nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
+          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+          ##[ ##1: #H1; #H2; nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (list_destruct_2 T … H3));
@@ -219,11 +236,15 @@ nlemma list_destruct
                    nnormalize; #H2; nrewrite > H2 in H1:(%);
                    nnormalize; #H1; napply (H1 (refl_eq …))
           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
-                   nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
           ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
-                   nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+                   nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H2;     
                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
@@ -267,7 +288,7 @@ nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_emp
  ncases l;
  nnormalize;
  ##[ ##1: #H; napply I
- ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+ ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -275,7 +296,7 @@ nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true 
  #T; #l;
  ncases l;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##2: #x; #l; #H; napply I
  ##]
 nqed.
@@ -310,9 +331,11 @@ nlemma symmetric_foldrightnelist2_aux
           ##| ##2: #h1; #l; ncases l;
                    ##[ ##1: #h3; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S O) = (S (S O)));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
                    ##| ##2: #h3; #l3; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
                    ##]                   
           ##]
@@ -320,9 +343,11 @@ nlemma symmetric_foldrightnelist2_aux
           ##[ ##1: #h4; ncases l3;
                    ##[ ##1: #h5; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S (S O)) = (S O));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
                    ##| ##2: #h5; #l5; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
                    ##]
           ##| ##2: #h4; #l4; #H1; #H2; #H3;
@@ -374,10 +399,10 @@ nlemma bfoldrightnelist2_to_eq
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
-          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##[ ##1: #hh2; #H1; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
           ##| ##2: #hh2; #ll2; #H1; #H2;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
                    nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
@@ -397,10 +422,14 @@ nlemma eq_to_bfoldrightnelist2
           ##[ ##1: #hh2; #H; #H1; nnormalize;
                    nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
                    napply refl_eq
-          ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
+          ##| ##2: #hh2; #ll2; #H; #H1;
+                   (* !!! ndestruct: assert false *)
+                   nelim (nelist_destruct_nil_cons ???? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
+          ##[ ##1: #hh2; #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   nelim (nelist_destruct_cons_nil ???? H2)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
                    nrewrite > (nelist_destruct_cons_cons_1 … H2);
                    nrewrite > (H1 hh2 hh2 (refl_eq …));
@@ -417,10 +446,10 @@ nlemma bfoldrightnelist2_to_lennelist
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
-          ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
+          ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
           ##]
  ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
+          ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
           ##| ##2: #hh2; #tt2; #H1; nnormalize;
                    nrewrite > (H tt2 ?);
                    ##[ ##1: napply refl_eq
@@ -440,11 +469,15 @@ nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T
                             #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
                    ##]
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1)
+                   nnormalize; #H1;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H1)
           ##]
  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
           ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H2)
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
@@ -467,10 +500,14 @@ nlemma nbfoldrightnelist2_to_neq
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
-          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
@@ -499,11 +536,15 @@ nlemma nelist_destruct
                             ##]
                    ##]
           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
-                   nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
           ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
-                   nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+                   nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H2;     
                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma
index 12ca65afe..fe976cba6 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
index 64eeb50f1..06ace91b2 100644
--- a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -35,6 +35,7 @@ nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
  #n; #H;
  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
@@ -43,6 +44,7 @@ nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
  #n; #H;
  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
@@ -58,12 +60,12 @@ nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
           nelim n2;
           nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
+          ##| ##2: #n3; #H; #H1; ndestruct (*nelim (nat_destruct_0_S ? H1)*)
           ##]
  ##| ##2: #n2; #H; #n3; #H1;
           ncases n3 in H1:(%) ⊢ %;
           nnormalize;
-          ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
+          ##[ ##1: #H1; ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
           ##| ##2: #n4; #H1;
                    napply (H n4 (nat_destruct_S_S … H1))
           ##]
@@ -85,12 +87,12 @@ nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
           nelim n2;
           nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1) 
+          ##| ##2: #n3; #H; #H1; ndestruct (*napply (bool_destruct … (O = S n3) H1)*)
           ##]
  ##| ##2: #n2; #H; #n3; #H1;
           ncases n3 in H1:(%) ⊢ %;
           nnormalize;
-          ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1)
+          ##[ ##1: #H1; ndestruct (*napply (bool_destruct … (S n2 = O) H1)*)
           ##| ##2: #n4; #H1;
                    nrewrite > (H n4 H1);
                    napply refl_eq
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
index e7665864f..6bd7fc4ae 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/option.ma b/helm/software/matita/contribs/ng_assembly/common/option.ma
index 0b71c17e4..244f087f3 100644
--- a/helm/software/matita/contribs/ng_assembly/common/option.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/option.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
index c8942ae6c..144733fe9 100644
--- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -35,6 +35,7 @@ nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
  #T; #x; #H;
  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
@@ -43,6 +44,7 @@ nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  #T; #x; #H;
  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
@@ -76,8 +78,12 @@ nlemma eq_to_eqoption :
  nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
- ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
- ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##2: #a; #H1;
+         (* !!! ndestruct: assert false *)
+         nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1;
+          (* !!! ndestruct: assert false *)
+          nelim (option_destruct_some_none ?? H1)
  ##| ##4: #a; #a0; #H1;
           nrewrite > (H … (option_destruct_some_some … H1));
           napply refl_eq
@@ -93,7 +99,7 @@ nlemma eqoption_to_eq :
  nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
- ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
+ ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
  ##| ##4: #a; #a0; #H1;
           nrewrite > (H … H1);
           napply refl_eq
@@ -105,14 +111,19 @@ nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.
  ##[ ##1: #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1; napply (option_destruct_none_some T … H1)
+                   nnormalize; #H1;
+                   (* !!! ndestruct: assert false *)
+                   napply (option_destruct_none_some T … H1)
           ##]
  ##| ##2: #xx; #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2; napply (option_destruct_some_none T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (option_destruct_some_none T … H2)
           ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                            nnormalize; #H2; napply (H1 (option_destruct_some_some T … H2))
+                            nnormalize; #H2;
+                            napply (H1 (option_destruct_some_some T … H2))
                    ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
                             nrewrite > H1; napply refl_eq
                    ##]
@@ -144,11 +155,16 @@ nlemma neqoption_to_neq :
  (eq_option T op1 op2 f = false → op1 ≠ op2).
  #T; #op1; nelim op1;
  ##[ ##1: #op2; ncases op2;
-          ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
-          ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)
+          ##[ ##1: nnormalize; #f; #H; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
+          ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (option_destruct_none_some T … H2)
           ##]
  ##| ##2: #xx; #op2; ncases op2;
-          ##[ ##1: nnormalize; #f; #H; #H1; #H2; napply (option_destruct_some_none T … H2)
+          ##[ ##1: nnormalize; #f; #H; #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (option_destruct_some_none T … H2)
           ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
                    napply (option_destruct_some_some T … H2)
           ##]
diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma
index 5be106fcb..fca58bc22 100644
--- a/helm/software/matita/contribs/ng_assembly/common/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -38,9 +38,8 @@ ndefinition snd ≝
 ndefinition eq_pair ≝
 λT1,T2:Type.λp1,p2:ProdT T1 T2.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
- match p1 with [ pair x1 y1 ⇒
-  match p2 with [ pair x2 y2 ⇒
-   (f1 x1 x2) ⊗ (f2 y1 y2) ]].
+ (f1 (fst … p1) (fst … p2)) ⊗
+ (f2 (snd … p1) (snd … p2)).
 
 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
@@ -57,9 +56,9 @@ ndefinition thd3T ≝
 ndefinition eq_triple ≝
 λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
- match p1 with [ triple x1 y1 z1 ⇒
-  match p2 with [ triple x2 y2 z2 ⇒
-   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
+ (f1 (fst3T … p1) (fst3T … p2)) ⊗
+ (f2 (snd3T … p1) (snd3T … p2)) ⊗
+ (f3 (thd3T … p1) (thd3T … p2)).
 
 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
@@ -79,9 +78,10 @@ ndefinition fth4T ≝
 ndefinition eq_quadruple ≝
 λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
- match p1 with [ quadruple x1 y1 z1 w1 ⇒
-  match p2 with [ quadruple x2 y2 z2 w2 ⇒
-   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
+ (f1 (fst4T … p1) (fst4T … p2)) ⊗
+ (f2 (snd4T … p1) (snd4T … p2)) ⊗
+ (f3 (thd4T … p1) (thd4T … p2)) ⊗
+ (f4 (fth4T … p1) (fth4T … p2)).
 
 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
@@ -95,15 +95,17 @@ ndefinition snd5T ≝
 ndefinition thd5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
 
-ndefinition frth5T ≝
+ndefinition fth5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
 
-ndefinition ffth5T ≝
+ndefinition fft5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
 
 ndefinition eq_quintuple ≝
 λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
- match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
-  match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
-   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].
+ (f1 (fst5T … p1) (fst5T … p2)) ⊗
+ (f2 (snd5T … p1) (snd5T … p2)) ⊗
+ (f3 (thd5T … p1) (thd5T … p2)) ⊗
+ (f4 (fth5T … p1) (fth5T … p2)) ⊗
+ (f5 (fft5T … p1) (fft5T … p2)).
diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
index b73d1347f..29998a836 100644
--- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -101,7 +101,7 @@ nlemma eqpair_to_eq :
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
  #H3;
- ##[ ##2: napply (bool_destruct … H3) ##]
+ ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
  #H4;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H2 y1 y2 H3);
@@ -282,11 +282,11 @@ nlemma eqtriple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H4; napply (bool_destruct … H4) ##]
+ ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
+ ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
  #H4; #H5; #H6;
  nrewrite > (H4 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -507,15 +507,15 @@ nlemma eqquadruple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H5; napply (bool_destruct … H5) ##]
+ ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
+ ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
+ ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
  #H5; #H6; #H7; #H8;
  nrewrite > (H5 (refl_eq …));
  nrewrite > (H6 (refl_eq …));
@@ -775,19 +775,19 @@ nlemma eqquintuple_to_eq :
  nletin K ≝ (H1 x1 x2);
  ncases (f1 x1 x2) in H:(%) K:(%);
  nnormalize;
- ##[ ##2: #H6; napply (bool_destruct … H6) ##]
+ ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
  nletin K1 ≝ (H2 y1 y2);
  ncases (f2 y1 y2) in K1:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
+ ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
  nletin K2 ≝ (H3 z1 z2);
  ncases (f3 z1 z2) in K2:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
+ ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
  nletin K3 ≝ (H4 v1 v2);
  ncases (f4 v1 v2) in K3:(%) ⊢ %;
  nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
  #H6; #H7; #H8; #H9; #H10;
  nrewrite > (H6 (refl_eq …));
  nrewrite > (H7 (refl_eq …));
diff --git a/helm/software/matita/contribs/ng_assembly/common/sigma.ma b/helm/software/matita/contribs/ng_assembly/common/sigma.ma
index 34ee411cd..529ca7ada 100755
--- a/helm/software/matita/contribs/ng_assembly/common/sigma.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/sigma.ma
@@ -16,13 +16,15 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
+include "common/theory.ma".
+
 (* coppia dipendente *)
 
-inductive sigma (A:Type) (P:A → Type) : Type ≝
+ninductive sigma (A:Type) (P:A → Type) : Type ≝
     sigma_intro: ∀x:A.P x → sigma A P.
 
 notation < "hvbox(\Sigma ident i opt (: tx) break . p)"
@@ -44,7 +46,7 @@ interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro ? c a
 
 interpretation "sigma" 'Sigma \eta.x = (sigma ? x).
 
-definition sigmaFst ≝
+ndefinition sigmaFst ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
-definition sigmaSnd ≝
+ndefinition sigmaSnd ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].
diff --git a/helm/software/matita/contribs/ng_assembly/common/string.ma b/helm/software/matita/contribs/ng_assembly/common/string.ma
index 7cf5ab73a..87ba11317 100644
--- a/helm/software/matita/contribs/ng_assembly/common/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/string.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
index be090076f..53dcc50d1 100755
--- a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index f96351775..bab796daa 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -16,13 +16,14 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
 
 (* ********************************** *)
 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
@@ -40,7 +41,6 @@ ndefinition Not: Prop → Prop ≝
 
 interpretation "logical not" 'not x = (Not x).
 
-(*
 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
@@ -178,6 +178,8 @@ ninductive Or2 (A,B:Prop) : Prop ≝
 
 interpretation "logical or" 'or x y = (Or2 x y).
 
+ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
+
 nlemma or2_elim
  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
  #P1; #P2; #Q; #H; #f1; #f2;
@@ -438,22 +440,18 @@ interpretation "exists" 'exists x = (ex ? x).
 
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
-*)
 
 (* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
-λA:Type.A → A → Prop. 
+λA.A → A → Prop. 
 
-(*
 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x:A.R x x.
-*)
 
 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → R y x.
 
-(*
 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 
@@ -468,18 +466,18 @@ ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 
 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → ¬ (R y x).
-*)
 
 (* logic/equality.ma *)
 
 ninductive eq (A:Type) (x:A) : A → Prop ≝
  refl_eq : eq A x x.
 
+ndefinition refl ≝ refl_eq.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
-(*
 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
  #T1; #T2; #x; #y; #f; #H;
  nrewrite < H;
@@ -498,7 +496,6 @@ nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) 
  nnormalize; #H; #H1;
  napply (H (eq_f … H1)).
 nqed.
-*)
 
 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
@@ -508,13 +505,92 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply refl_eq.
 nqed.
 
-nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
  nrewrite < (symmetric_eq … H1);
  napply H.
 nqed.
 
-(*
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
+
+ndefinition R1 ≝ eq_rect_Type0.
+
+ndefinition R2 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  T2 b0 e0 b1 e1.
+ #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
+ napply (eq_rect_Type0 ????? e1);
+ napply (R1 ?? ? ?? e0);
+ napply a2;
+nqed.
+
+ndefinition R3 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
+ napply (eq_rect_Type0 ????? e2);
+ napply (R2 ?? ? ???? e0 ? e1);
+ napply a3;
+nqed.
+
+ndefinition R4 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+      Type[0].
+  ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2) 
+      a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+                   a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
+                   a3).
+  ∀b0:T0.
+  ∀e0:eq (T0 …) a0 b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀b3: T3 b0 e0 b1 e1 b2 e2.
+  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  T4 b0 e0 b1 e1 b2 e2 b3 e3.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+ napply (eq_rect_Type0 ????? e3);
+ napply (R3 ????????? e0 ? e1 ? e2);
+ napply a4;
+nqed.
+
 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
  #T; #x; #y;
  nnormalize;
@@ -531,12 +607,3 @@ ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 
 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
-*)
-
-ninductive bool : Type ≝
- true : bool |
- false : bool.
-
-nlemma pippo : (true = false) → (false = true).
- #H; ndestruct.
-nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index d69d373ee..a897995c2 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -68,7 +68,7 @@ common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
 num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
 freescale/opcode_base_lemmas_opcode.ma freescale/opcode_base.ma num/bool_lemmas.ma
 freescale_tests/micro_tests4.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-common/sigma.ma 
+common/sigma.ma common/theory.ma
 common/list_lemmas.ma common/list.ma
 universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma
 num/bitrigesim.ma num/bool.ma
diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
index 18dcce4b7..fdfb9fbd2 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
index 5eecaff91..021563e94 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* BITRIGESIMALI *)
 (* ************* *)
 
+(*
 ndefinition bitrigesim_destruct_aux ≝
 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
  match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
  #n1; #n2; #H;
@@ -55,38 +57,38 @@ nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
  ##]
 nqed.
 
-nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
-nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] nqed.
+nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2. #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2. #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2. #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2. #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2. #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2. #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
+nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2. #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: ndestruct (*napply (bool_destruct … H)*) ##] nqed.
 
 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
  #t1; ncases t1;
diff --git a/helm/software/matita/contribs/ng_assembly/num/bool.ma b/helm/software/matita/contribs/ng_assembly/num/bool.ma
index a878b98af..8092713f2 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bool.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index fddf6d832..db5214c6d 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -26,7 +26,8 @@ include "num/bool.ma".
 (* BOOLEANI *)
 (* ******** *)
 
-(*ndefinition bool_destruct_aux ≝
+(*
+ndefinition bool_destruct_aux ≝
 Πb1,b2:bool.ΠP:Prop.b1 = b2 →
  match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
 
@@ -36,7 +37,8 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b1;
  nnormalize;
  napply (λx.x).
-nqed.*)
+nqed.
+*)
 
 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  #b1; #b2;
@@ -113,7 +115,7 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
  ncases b2;
  nnormalize;
  ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -126,7 +128,7 @@ nlemma decidable_bool : ∀x,y:bool.decidable (x = y).
  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
           nnormalize; #H;
           napply False_ind;
-          napply (bool_destruct … H)
+          ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -142,8 +144,8 @@ nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1,4: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (bool_destruct … H1)
+ ##[ ##1,4: #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##*: #H; #H1; ndestruct (*napply (bool_destruct … H1)*)
  ##]
 nqed.
 
@@ -159,15 +161,15 @@ nqed.
 
 nlemma eqfalse_to_neqtrue : ∀x.x = false → x ≠ true.
  #x; nelim x;
- ##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##2: #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
  ##]
 nqed.
 
 nlemma eqtrue_to_neqfalse : ∀x.x = true → x ≠ false.
  #x; nelim x;
- ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
- ##| ##2: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -191,7 +193,7 @@ nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  ncases b2;
  nnormalize;
  ##[ ##1,2: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -201,7 +203,7 @@ nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
  ncases b2;
  nnormalize;
  ##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -212,7 +214,7 @@ nlemma andb_false2
  ncases b1;
  ncases b2;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##2,4: #H; napply (or2_intro2 … H)
  ##| ##3: #H; napply (or2_intro1 … H)
  ##]
@@ -226,7 +228,7 @@ nlemma andb_false3
  ncases b2;
  ncases b3;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##5,6,7,8: #H; napply (or3_intro1 … H)
  ##| ##2,4: #H; napply (or3_intro3 … H)
  ##| ##3: #H; napply (or3_intro2 … H)
@@ -242,7 +244,7 @@ nlemma andb_false4
  ncases b3;
  ncases b4;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##9,10,11,12,13,14,15,16: #H; napply (or4_intro1 … H)
  ##| ##5,6,7,8: #H; napply (or4_intro2 … H)
  ##| ##3,4: #H; napply (or4_intro3 … H)
@@ -260,7 +262,7 @@ nlemma andb_false5
  ncases b4;
  ncases b5;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #H; napply (or5_intro1 … H)
  ##| ##9,10,11,12,13,14,15,16: #H; napply (or5_intro2 … H)
  ##| ##5,6,7,8: #H; napply (or5_intro3 … H)
@@ -307,7 +309,7 @@ nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
  ncases b2;
  nnormalize;
  ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -317,6 +319,6 @@ nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
  ncases b2;
  nnormalize;
  ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index 4d621bb29..e899a6989 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
index 38c472806..10a100965 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index eb92c8f2d..f4728367f 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
index 6e4d25e1e..c6e09d5ce 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* ESADECIMALI *)
 (* *********** *)
 
+(*
 ndefinition exadecim_destruct_aux ≝
 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ ndefinition exadecim_destruct : exadecim_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
  #e1; #e2;
@@ -314,7 +316,7 @@ nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
  ncases n2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/oct.ma b/helm/software/matita/contribs/ng_assembly/num/oct.ma
index 479a1ca82..fbdbacd5d 100755
--- a/helm/software/matita/contribs/ng_assembly/num/oct.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
index d6c014598..3a29cc1b7 100755
--- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* OTTALI *)
 (* ****** *)
 
+(*
 ndefinition oct_destruct_aux ≝
 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  match eq_oct n1 n2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ ndefinition oct_destruct : oct_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
  #n1; #n2; #H;
@@ -61,7 +63,7 @@ nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
  ncases n2;
  nnormalize;
  ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern.ma b/helm/software/matita/contribs/ng_assembly/num/quatern.ma
index af321ea1d..a6bc1343f 100755
--- a/helm/software/matita/contribs/ng_assembly/num/quatern.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/quatern.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
index c2c8a3399..a3ff94559 100755
--- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* QUATERNARI *)
 (* ********** *)
 
+(*
 ndefinition quatern_destruct_aux ≝
 Πn1,n2:quatern.ΠP:Prop.n1 = n2 →
  match eq_qu n1 n2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ ndefinition quatern_destruct : quatern_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
  #n1; #n2; #H;
@@ -61,7 +63,7 @@ nlemma eqqu_to_eq : ∀n1,n2.eq_qu n1 n2 = true → n1 = n2.
  ncases n2;
  nnormalize;
  ##[ ##1,6,11,16: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 51fb30644..2ae8fc5fd 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
index 56a54ae99..2e38a06fc 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index a5a74faa8..416ad623f 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
diff --git a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
index 5f42bbc7b..026086d8f 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
-- 
2.39.2