From 3e5c359c75874748cfed8a9046031b62396e0e6d Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Sun, 12 Jul 2009 00:57:09 +0000
Subject: [PATCH]

---
 .../matita/contribs/ng_assembly/depends       |   1 +
 .../ng_assembly/freescale/aux_bases.ma        | 371 ++++++++++
 .../ng_assembly/freescale/aux_bases_lemmas.ma | 672 ++++++++++++++++++
 3 files changed, 1044 insertions(+)
 create mode 100755 helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
 create mode 100755 helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index 3a30fbcd1..bec7a1b91 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -7,6 +7,7 @@ freescale/byte8_lemmas.ma freescale/byte8.ma freescale/exadecim_lemmas.ma
 freescale/pts.ma 
 freescale/option_lemmas.ma freescale/bool_lemmas.ma freescale/option.ma
 freescale/prod_lemmas.ma freescale/bool_lemmas.ma freescale/prod.ma
+freescale/aux_bases.ma freescale/bool.ma freescale/nat.ma
 freescale/nat.ma freescale/bool.ma freescale/pts.ma
 freescale/word32.ma freescale/word16.ma
 freescale/word16.ma freescale/byte8.ma
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
new file mode 100755
index 000000000..2e71ab1b7
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
@@ -0,0 +1,371 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                           Progetto FreeScale                           *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool.ma".
+include "freescale/nat.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ninductive oct : Type ≝
+  o0: oct
+| o1: oct
+| o2: oct
+| o3: oct
+| o4: oct
+| o5: oct
+| o6: oct
+| o7: oct.
+
+ndefinition oct_ind :
+ ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Prop.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. 
+
+ndefinition oct_rec :
+ ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Set.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. 
+
+ndefinition oct_rect :
+ ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Type.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
+
+(* operatore = *)
+ndefinition eq_oct ≝
+λn1,n2:oct.
+ match n1 with
+  [ o0 ⇒ match n2 with
+   [ o0 ⇒ true  | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ] 
+  | o1 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ true  | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ] 
+  | o2 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ true  | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ] 
+  | o3 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ true
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ] 
+  | o4 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ true  | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ] 
+  | o5 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ true  | o6 ⇒ false | o7 ⇒ false ] 
+  | o6 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ true  | o7 ⇒ false ] 
+  | o7 ⇒ match n2 with
+   [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+   | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ true  ] 
+  ].
+
+(* ottali → naturali *)
+ndefinition nat_of_oct ≝
+λn:oct.
+ match n with
+  [ o0 ⇒ 0 | o1 ⇒ 1 | o2 ⇒ 2  | o3 ⇒ 3  | o4 ⇒ 4  | o5 ⇒ 5  | o6 ⇒ 6  | o7 ⇒ 7 ].
+
+(* iteratore sugli ottali *)
+ndefinition forall_oct ≝ λP.
+ P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ninductive bitrigesim : Type ≝
+  t00: bitrigesim
+| t01: bitrigesim
+| t02: bitrigesim
+| t03: bitrigesim
+| t04: bitrigesim
+| t05: bitrigesim
+| t06: bitrigesim
+| t07: bitrigesim
+| t08: bitrigesim
+| t09: bitrigesim
+| t0A: bitrigesim
+| t0B: bitrigesim
+| t0C: bitrigesim
+| t0D: bitrigesim
+| t0E: bitrigesim
+| t0F: bitrigesim
+| t10: bitrigesim
+| t11: bitrigesim
+| t12: bitrigesim
+| t13: bitrigesim
+| t14: bitrigesim
+| t15: bitrigesim
+| t16: bitrigesim
+| t17: bitrigesim
+| t18: bitrigesim
+| t19: bitrigesim
+| t1A: bitrigesim
+| t1B: bitrigesim
+| t1C: bitrigesim
+| t1D: bitrigesim
+| t1E: bitrigesim
+| t1F: bitrigesim.
+
+ndefinition bitrigesim_ind :
+ ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+                      P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+                      P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+                      P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
+λP:bitrigesim → Prop.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
+  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].    
+
+ndefinition bitrigesim_rec :
+ ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+                     P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+                     P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+                     P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
+λP:bitrigesim → Set.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
+  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
+
+ndefinition bitrigesim_rect :
+ ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+                      P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+                      P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+                      P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
+λP:bitrigesim → Type.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
+  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
+
+(* operatore = *)
+ndefinition eq_bitrig ≝
+λt1,t2:bitrigesim.
+ match t1 with
+  [ t00 ⇒ match t2 with
+   [ t00 ⇒ true  | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t01 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ true  | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t02 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ true  | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t03 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ true  | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t04 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ true  | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t05 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ true  | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t06 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ true  | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t07 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ true
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t08 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ true  | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t09 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ true  | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0A ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ true  | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0B ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ true  | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0C ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ true  | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0D ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ true  | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0E ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ true  | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t0F ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ true
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t10 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ true  | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t11 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ true  | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t12 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ true  | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t13 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ true  | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t14 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ true  | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t15 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ true  | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t16 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ true  | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t17 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ true
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t18 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ true  | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t19 ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ true  | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t1A ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ true  | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t1B ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ true  | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t1C ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ true  | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+  | t1D ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ true  | t1E ⇒ false | t1F ⇒ false ]
+  | t1E ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ true  | t1F ⇒ false ]
+  | t1F ⇒ match t2 with
+   [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+   | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+   | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+   | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ true  ]                                               
+  ].
+
+(* bitrigesimali → naturali *)
+ndefinition nat_of_bitrigesim ≝
+λt:bitrigesim.
+ match t with
+  [ t00 ⇒ 0  | t01 ⇒ 1  | t02 ⇒ 2  | t03 ⇒ 3  | t04 ⇒ 4  | t05 ⇒ 5  | t06 ⇒ 6  | t07 ⇒ 7
+  | t08 ⇒ 8  | t09 ⇒ 9  | t0A ⇒ 10 | t0B ⇒ 11 | t0C ⇒ 12 | t0D ⇒ 13 | t0E ⇒ 14 | t0F ⇒ 15
+  | t10 ⇒ 16 | t11 ⇒ 17 | t12 ⇒ 18 | t13 ⇒ 19 | t14 ⇒ 20 | t15 ⇒ 21 | t16 ⇒ 22 | t17 ⇒ 23
+  | t18 ⇒ 24 | t19 ⇒ 25 | t1A ⇒ 26 | t1B ⇒ 27 | t1C ⇒ 28 | t1D ⇒ 29 | t1E ⇒ 30 | t1F ⇒ 31 ].
+
+(* iteratore sui bitrigesimali *)
+ndefinition forall_bitrigesim ≝ λP.
+ P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
+ P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
+ P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
+ P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
new file mode 100755
index 000000000..c85df6e61
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
@@ -0,0 +1,672 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                           Progetto FreeScale                           *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/aux_bases.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ndefinition oct_destruct :
+ Πn1,n2:oct.ΠP:Prop.n1 = n2 →
+ match n1 with
+  [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
+  | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
+  | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
+  | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
+  | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
+  | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
+  | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
+  | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
+  ].
+ #n1; #n2; #P;
+ nelim n1;
+ ##[ ##1: nelim n2; nnormalize; #H;
+          ##[ ##1: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##2: nelim n2; nnormalize; #H;
+          ##[ ##2: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##3: nelim n2; nnormalize; #H;
+          ##[ ##3: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##4: nelim n2; nnormalize; #H;
+          ##[ ##4: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##5: nelim n2; nnormalize; #H;
+          ##[ ##5: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##6: nelim n2; nnormalize; #H;
+          ##[ ##6: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##7: nelim n2; nnormalize; #H;
+          ##[ ##7: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##8: nelim n2; nnormalize; #H;
+          ##[ ##8: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
+ #n1; #n2;
+ nelim n1;
+ nelim n2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
+ #n1; #n2; #H;
+ nletin K ≝ (bool_destruct ?? (n1 = n2) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
+ #n1; #n2; #H;
+ nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ndefinition bitrigesim_destruct :
+ Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
+ match t1 with
+  [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
+  | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
+  | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
+  | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
+  | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
+  | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
+  | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
+  | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
+  | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
+  | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
+  | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
+  | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
+  | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
+  | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
+  | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
+  | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
+  | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
+  | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
+  | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
+  | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
+  | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
+  | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
+  | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
+  | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
+  | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
+  | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
+  | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
+  | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
+  | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
+  | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
+  | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
+  | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
+  ].
+ #t1; #t2; #P;
+ nelim t1;
+ ##[ ##1: nelim t2; nnormalize; #H;
+          ##[ ##1: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+          ##[ ##2: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+          ##[ ##3: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+          ##[ ##4: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+          ##[ ##5: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+          ##[ ##6: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+          ##[ ##7: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+          ##[ ##8: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+          ##[ ##9: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+          ##[ ##10: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+          ##[ ##11: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+          ##[ ##12: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+          ##[ ##13: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+          ##[ ##14: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+          ##[ ##15: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+          ##[ ##16: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+          ##[ ##17: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+          ##[ ##18: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+          ##[ ##19: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+          ##[ ##20: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+          ##[ ##21: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+          ##[ ##22: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+          ##[ ##23: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+          ##[ ##24: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+          ##[ ##25: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+          ##[ ##26: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+          ##[ ##27: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+          ##[ ##28: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+          ##[ ##29: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+          ##[ ##30: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+          ##[ ##31: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+          ##[ ##32: napply (λx:P.x)
+          ##| ##*: napply (False_ind ??);
+                   nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
+                   nrewrite > H; nnormalize; napply I
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
+ #t1;
+ nelim t1;
+ ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
+ #t1; #t2; #H;
+ nletin K ≝ (bool_destruct ?? (t1 = t2) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+          ##[ ##1: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+          ##[ ##2: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]          
+ ##| ##3: nelim t2; nnormalize; #H;
+          ##[ ##3: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+          ##[ ##4: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+          ##[ ##5: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+          ##[ ##6: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+          ##[ ##7: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+          ##[ ##8: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+          ##[ ##9: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+          ##[ ##10: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+          ##[ ##11: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##12: nelim t2; nnormalize; #H;
+          ##[ ##12: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+          ##[ ##13: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+          ##[ ##14: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+          ##[ ##15: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##16: nelim t2; nnormalize; #H;
+          ##[ ##16: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+          ##[ ##17: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+          ##[ ##18: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+          ##[ ##19: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##20: nelim t2; nnormalize; #H;
+          ##[ ##20: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+          ##[ ##21: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+          ##[ ##22: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+          ##[ ##23: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+          ##[ ##24: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+          ##[ ##25: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+          ##[ ##26: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+          ##[ ##27: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+          ##[ ##28: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+          ##[ ##29: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+          ##[ ##30: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+          ##[ ##31: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+          ##[ ##32: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##]
+nqed.
+
+nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
+ #t1; #t2; #H;
+ nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+          ##[ ##1: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+          ##[ ##2: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]          
+ ##| ##3: nelim t2; nnormalize; #H;
+          ##[ ##3: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+          ##[ ##4: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+          ##[ ##5: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+          ##[ ##6: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+          ##[ ##7: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+          ##[ ##8: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+          ##[ ##9: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+          ##[ ##10: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+          ##[ ##11: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##12: nelim t2; nnormalize; #H;
+          ##[ ##12: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+          ##[ ##13: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+          ##[ ##14: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+          ##[ ##15: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##16: nelim t2; nnormalize; #H;
+          ##[ ##16: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+          ##[ ##17: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+          ##[ ##18: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+          ##[ ##19: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]            
+ ##| ##20: nelim t2; nnormalize; #H;
+          ##[ ##20: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+          ##[ ##21: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+          ##[ ##22: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+          ##[ ##23: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+          ##[ ##24: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+          ##[ ##25: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+          ##[ ##26: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+          ##[ ##27: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+          ##[ ##28: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+          ##[ ##29: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+          ##[ ##30: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+          ##[ ##31: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+          ##[ ##32: napply (refl_eq ??)
+          ##| ##*: napply H
+          ##]
+ ##]
+nqed.
-- 
2.39.2