--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+ninductive ascii : Type ≝
+(* numeri *)
+ ch_0: ascii
+| ch_1: ascii
+| ch_2: ascii
+| ch_3: ascii
+| ch_4: ascii
+| ch_5: ascii
+| ch_6: ascii
+| ch_7: ascii
+| ch_8: ascii
+| ch_9: ascii
+
+(* simboli *)
+| ch__: ascii
+
+(* maiuscole *)
+| ch_A: ascii
+| ch_B: ascii
+| ch_C: ascii
+| ch_D: ascii
+| ch_E: ascii
+| ch_F: ascii
+| ch_G: ascii
+| ch_H: ascii
+| ch_I: ascii
+| ch_J: ascii
+| ch_K: ascii
+| ch_L: ascii
+| ch_M: ascii
+| ch_N: ascii
+| ch_O: ascii
+| ch_P: ascii
+| ch_Q: ascii
+| ch_R: ascii
+| ch_S: ascii
+| ch_T: ascii
+| ch_U: ascii
+| ch_V: ascii
+| ch_W: ascii
+| ch_X: ascii
+| ch_Y: ascii
+| ch_Z: ascii
+
+(* minuscole *)
+| ch_a: ascii
+| ch_b: ascii
+| ch_c: ascii
+| ch_d: ascii
+| ch_e: ascii
+| ch_f: ascii
+| ch_g: ascii
+| ch_h: ascii
+| ch_i: ascii
+| ch_j: ascii
+| ch_k: ascii
+| ch_l: ascii
+| ch_m: ascii
+| ch_n: ascii
+| ch_o: ascii
+| ch_p: ascii
+| ch_q: ascii
+| ch_r: ascii
+| ch_s: ascii
+| ch_t: ascii
+| ch_u: ascii
+| ch_v: ascii
+| ch_w: ascii
+| ch_x: ascii
+| ch_y: ascii
+| ch_z: ascii.
+
+(* confronto fra ascii *)
+ndefinition eq_ascii ≝
+λc,c':ascii.match c with
+ [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ]
+ | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ]
+ | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ]
+ | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ]
+ | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ]
+ | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ]
+ | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ]
+ | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ]
+ | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ]
+ | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ]
+ | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ]
+ | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ]
+ | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ]
+ | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ]
+ | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ]
+ | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ]
+ | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ]
+ | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ]
+ | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ]
+ | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ]
+ | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ]
+ | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ]
+ | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ]
+ | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ]
+ | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ]
+ | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ]
+ | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ]
+ | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ]
+ | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ]
+ | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ]
+ | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ]
+ | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ]
+ | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ]
+ | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ]
+ | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ]
+ | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ]
+ | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ]
+ | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ]
+ | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ]
+ | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ]
+ | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ]
+ | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ]
+ | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ]
+ | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ]
+ | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ]
+ | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ]
+ | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ]
+ | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ]
+ | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ]
+ | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ]
+ | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ]
+ | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ]
+ | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ]
+ | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ]
+ | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ]
+ | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ]
+ | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ]
+ | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ]
+ | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ]
+ | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ]
+ | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ]
+ | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ]
+ | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/ascii.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##1: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##2: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##3: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##4: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##5: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##6: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##7: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##8: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##9: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##10: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##11: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##12: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##13: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##14: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##15: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##16: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##17: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##18: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##19: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##20: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##21: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##22: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##23: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##24: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##25: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##26: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##27: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##28: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##29: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##30: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##31: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##32: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##33: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##34: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##35: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##36: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##37: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##38: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##39: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##40: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##41: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##42: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##43: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##44: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##45: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##46: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##47: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##48: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##49: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##50: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##51: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##52: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##53: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##54: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##55: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##56: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##57: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##58: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##59: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##60: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##61: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##62: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ].
+ #c2; #P; ncases c2; nnormalize;
+ ##[ ##63: #H; napply (λx:P.x)
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition ascii_destruct_aux ≝
+Πc1,c2.ΠP:Prop.c1 = c2 →
+ match c1 with
+ [ ch_0 ⇒ match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ] | ch_1 ⇒ match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ]
+ | ch_2 ⇒ match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ] | ch_3 ⇒ match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ]
+ | ch_4 ⇒ match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ] | ch_5 ⇒ match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ]
+ | ch_6 ⇒ match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ] | ch_7 ⇒ match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ]
+ | ch_8 ⇒ match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ] | ch_9 ⇒ match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ]
+ | ch__ ⇒ match c2 with [ ch__ ⇒ P → P | _ ⇒ P ] | ch_A ⇒ match c2 with [ ch_A ⇒ P → P | _ ⇒ P ]
+ | ch_B ⇒ match c2 with [ ch_B ⇒ P → P | _ ⇒ P ] | ch_C ⇒ match c2 with [ ch_C ⇒ P → P | _ ⇒ P ]
+ | ch_D ⇒ match c2 with [ ch_D ⇒ P → P | _ ⇒ P ] | ch_E ⇒ match c2 with [ ch_E ⇒ P → P | _ ⇒ P ]
+ | ch_F ⇒ match c2 with [ ch_F ⇒ P → P | _ ⇒ P ] | ch_G ⇒ match c2 with [ ch_G ⇒ P → P | _ ⇒ P ]
+ | ch_H ⇒ match c2 with [ ch_H ⇒ P → P | _ ⇒ P ] | ch_I ⇒ match c2 with [ ch_I ⇒ P → P | _ ⇒ P ]
+ | ch_J ⇒ match c2 with [ ch_J ⇒ P → P | _ ⇒ P ] | ch_K ⇒ match c2 with [ ch_K ⇒ P → P | _ ⇒ P ]
+ | ch_L ⇒ match c2 with [ ch_L ⇒ P → P | _ ⇒ P ] | ch_M ⇒ match c2 with [ ch_M ⇒ P → P | _ ⇒ P ]
+ | ch_N ⇒ match c2 with [ ch_N ⇒ P → P | _ ⇒ P ] | ch_O ⇒ match c2 with [ ch_O ⇒ P → P | _ ⇒ P ]
+ | ch_P ⇒ match c2 with [ ch_P ⇒ P → P | _ ⇒ P ] | ch_Q ⇒ match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ]
+ | ch_R ⇒ match c2 with [ ch_R ⇒ P → P | _ ⇒ P ] | ch_S ⇒ match c2 with [ ch_S ⇒ P → P | _ ⇒ P ]
+ | ch_T ⇒ match c2 with [ ch_T ⇒ P → P | _ ⇒ P ] | ch_U ⇒ match c2 with [ ch_U ⇒ P → P | _ ⇒ P ]
+ | ch_V ⇒ match c2 with [ ch_V ⇒ P → P | _ ⇒ P ] | ch_W ⇒ match c2 with [ ch_W ⇒ P → P | _ ⇒ P ]
+ | ch_X ⇒ match c2 with [ ch_X ⇒ P → P | _ ⇒ P ] | ch_Y ⇒ match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ]
+ | ch_Z ⇒ match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ] | ch_a ⇒ match c2 with [ ch_a ⇒ P → P | _ ⇒ P ]
+ | ch_b ⇒ match c2 with [ ch_b ⇒ P → P | _ ⇒ P ] | ch_c ⇒ match c2 with [ ch_c ⇒ P → P | _ ⇒ P ]
+ | ch_d ⇒ match c2 with [ ch_d ⇒ P → P | _ ⇒ P ] | ch_e ⇒ match c2 with [ ch_e ⇒ P → P | _ ⇒ P ]
+ | ch_f ⇒ match c2 with [ ch_f ⇒ P → P | _ ⇒ P ] | ch_g ⇒ match c2 with [ ch_g ⇒ P → P | _ ⇒ P ]
+ | ch_h ⇒ match c2 with [ ch_h ⇒ P → P | _ ⇒ P ] | ch_i ⇒ match c2 with [ ch_i ⇒ P → P | _ ⇒ P ]
+ | ch_j ⇒ match c2 with [ ch_j ⇒ P → P | _ ⇒ P ] | ch_k ⇒ match c2 with [ ch_k ⇒ P → P | _ ⇒ P ]
+ | ch_l ⇒ match c2 with [ ch_l ⇒ P → P | _ ⇒ P ] | ch_m ⇒ match c2 with [ ch_m ⇒ P → P | _ ⇒ P ]
+ | ch_n ⇒ match c2 with [ ch_n ⇒ P → P | _ ⇒ P ] | ch_o ⇒ match c2 with [ ch_o ⇒ P → P | _ ⇒ P ]
+ | ch_p ⇒ match c2 with [ ch_p ⇒ P → P | _ ⇒ P ] | ch_q ⇒ match c2 with [ ch_q ⇒ P → P | _ ⇒ P ]
+ | ch_r ⇒ match c2 with [ ch_r ⇒ P → P | _ ⇒ P ] | ch_s ⇒ match c2 with [ ch_s ⇒ P → P | _ ⇒ P ]
+ | ch_t ⇒ match c2 with [ ch_t ⇒ P → P | _ ⇒ P ] | ch_u ⇒ match c2 with [ ch_u ⇒ P → P | _ ⇒ P ]
+ | ch_v ⇒ match c2 with [ ch_v ⇒ P → P | _ ⇒ P ] | ch_w ⇒ match c2 with [ ch_w ⇒ P → P | _ ⇒ P ]
+ | ch_x ⇒ match c2 with [ ch_x ⇒ P → P | _ ⇒ P ] | ch_y ⇒ match c2 with [ ch_y ⇒ P → P | _ ⇒ P ]
+ | ch_z ⇒ match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]].
+
+nlemma ascii_destruct : ascii_destruct_aux.
+ #c1; ncases c1;
+ ##[ ##1: napply ascii_destruct1 ##| ##2: napply ascii_destruct2
+ ##| ##3: napply ascii_destruct3 ##| ##4: napply ascii_destruct4
+ ##| ##5: napply ascii_destruct5 ##| ##6: napply ascii_destruct6
+ ##| ##7: napply ascii_destruct7 ##| ##8: napply ascii_destruct8
+ ##| ##9: napply ascii_destruct9 ##| ##10: napply ascii_destruct10
+ ##| ##11: napply ascii_destruct11 ##| ##12: napply ascii_destruct12
+ ##| ##13: napply ascii_destruct13 ##| ##14: napply ascii_destruct14
+ ##| ##15: napply ascii_destruct15 ##| ##16: napply ascii_destruct16
+ ##| ##17: napply ascii_destruct17 ##| ##18: napply ascii_destruct18
+ ##| ##19: napply ascii_destruct19 ##| ##20: napply ascii_destruct20
+ ##| ##21: napply ascii_destruct21 ##| ##22: napply ascii_destruct22
+ ##| ##23: napply ascii_destruct23 ##| ##24: napply ascii_destruct24
+ ##| ##25: napply ascii_destruct25 ##| ##26: napply ascii_destruct26
+ ##| ##27: napply ascii_destruct27 ##| ##28: napply ascii_destruct28
+ ##| ##29: napply ascii_destruct29 ##| ##30: napply ascii_destruct30
+ ##| ##31: napply ascii_destruct31 ##| ##32: napply ascii_destruct32
+ ##| ##33: napply ascii_destruct33 ##| ##34: napply ascii_destruct34
+ ##| ##35: napply ascii_destruct35 ##| ##36: napply ascii_destruct36
+ ##| ##37: napply ascii_destruct37 ##| ##38: napply ascii_destruct38
+ ##| ##39: napply ascii_destruct39 ##| ##40: napply ascii_destruct40
+ ##| ##41: napply ascii_destruct41 ##| ##42: napply ascii_destruct42
+ ##| ##43: napply ascii_destruct43 ##| ##44: napply ascii_destruct44
+ ##| ##45: napply ascii_destruct45 ##| ##46: napply ascii_destruct46
+ ##| ##47: napply ascii_destruct47 ##| ##48: napply ascii_destruct48
+ ##| ##49: napply ascii_destruct49 ##| ##50: napply ascii_destruct50
+ ##| ##51: napply ascii_destruct51 ##| ##52: napply ascii_destruct52
+ ##| ##53: napply ascii_destruct53 ##| ##54: napply ascii_destruct54
+ ##| ##55: napply ascii_destruct55 ##| ##56: napply ascii_destruct56
+ ##| ##57: napply ascii_destruct57 ##| ##58: napply ascii_destruct58
+ ##| ##59: napply ascii_destruct59 ##| ##60: napply ascii_destruct60
+ ##| ##61: napply ascii_destruct61 ##| ##62: napply ascii_destruct62
+ ##| ##63: napply ascii_destruct63 ##]
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/ascii_lemmas1.ma".
+include "num/bool_lemmas.ma".
+
+(* ************************** *)
+(* DEFINIZIONE ASCII MINIMALE *)
+(* ************************** *)
+
+nlemma symmetric_eqascii1 : ∀a2.eq_ascii ch_0 a2 = eq_ascii a2 ch_0. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii2 : ∀a2.eq_ascii ch_1 a2 = eq_ascii a2 ch_1. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii3 : ∀a2.eq_ascii ch_2 a2 = eq_ascii a2 ch_2. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii4 : ∀a2.eq_ascii ch_3 a2 = eq_ascii a2 ch_3. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii5 : ∀a2.eq_ascii ch_4 a2 = eq_ascii a2 ch_4. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii6 : ∀a2.eq_ascii ch_5 a2 = eq_ascii a2 ch_5. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii7 : ∀a2.eq_ascii ch_6 a2 = eq_ascii a2 ch_6. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii8 : ∀a2.eq_ascii ch_7 a2 = eq_ascii a2 ch_7. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii9 : ∀a2.eq_ascii ch_8 a2 = eq_ascii a2 ch_8. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii10 : ∀a2.eq_ascii ch_9 a2 = eq_ascii a2 ch_9. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii11 : ∀a2.eq_ascii ch__ a2 = eq_ascii a2 ch__. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii12 : ∀a2.eq_ascii ch_A a2 = eq_ascii a2 ch_A. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii13 : ∀a2.eq_ascii ch_B a2 = eq_ascii a2 ch_B. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii14 : ∀a2.eq_ascii ch_C a2 = eq_ascii a2 ch_C. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii15 : ∀a2.eq_ascii ch_D a2 = eq_ascii a2 ch_D. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii16 : ∀a2.eq_ascii ch_E a2 = eq_ascii a2 ch_E. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii17 : ∀a2.eq_ascii ch_F a2 = eq_ascii a2 ch_F. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii18 : ∀a2.eq_ascii ch_G a2 = eq_ascii a2 ch_G. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii19 : ∀a2.eq_ascii ch_H a2 = eq_ascii a2 ch_H. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii20 : ∀a2.eq_ascii ch_I a2 = eq_ascii a2 ch_I. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii21 : ∀a2.eq_ascii ch_J a2 = eq_ascii a2 ch_J. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii22 : ∀a2.eq_ascii ch_K a2 = eq_ascii a2 ch_K. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii23 : ∀a2.eq_ascii ch_L a2 = eq_ascii a2 ch_L. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii24 : ∀a2.eq_ascii ch_M a2 = eq_ascii a2 ch_M. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii25 : ∀a2.eq_ascii ch_N a2 = eq_ascii a2 ch_N. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii26 : ∀a2.eq_ascii ch_O a2 = eq_ascii a2 ch_O. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii27 : ∀a2.eq_ascii ch_P a2 = eq_ascii a2 ch_P. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii28 : ∀a2.eq_ascii ch_Q a2 = eq_ascii a2 ch_Q. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii29 : ∀a2.eq_ascii ch_R a2 = eq_ascii a2 ch_R. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii30 : ∀a2.eq_ascii ch_S a2 = eq_ascii a2 ch_S. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii31 : ∀a2.eq_ascii ch_T a2 = eq_ascii a2 ch_T. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii32 : ∀a2.eq_ascii ch_U a2 = eq_ascii a2 ch_U. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii33 : ∀a2.eq_ascii ch_V a2 = eq_ascii a2 ch_V. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii34 : ∀a2.eq_ascii ch_W a2 = eq_ascii a2 ch_W. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii35 : ∀a2.eq_ascii ch_X a2 = eq_ascii a2 ch_X. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii36 : ∀a2.eq_ascii ch_Y a2 = eq_ascii a2 ch_Y. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii37 : ∀a2.eq_ascii ch_Z a2 = eq_ascii a2 ch_Z. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii38 : ∀a2.eq_ascii ch_a a2 = eq_ascii a2 ch_a. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii39 : ∀a2.eq_ascii ch_b a2 = eq_ascii a2 ch_b. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii40 : ∀a2.eq_ascii ch_c a2 = eq_ascii a2 ch_c. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii41 : ∀a2.eq_ascii ch_d a2 = eq_ascii a2 ch_d. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii42 : ∀a2.eq_ascii ch_e a2 = eq_ascii a2 ch_e. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii43 : ∀a2.eq_ascii ch_f a2 = eq_ascii a2 ch_f. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii44 : ∀a2.eq_ascii ch_g a2 = eq_ascii a2 ch_g. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii45 : ∀a2.eq_ascii ch_h a2 = eq_ascii a2 ch_h. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii46 : ∀a2.eq_ascii ch_i a2 = eq_ascii a2 ch_i. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii47 : ∀a2.eq_ascii ch_j a2 = eq_ascii a2 ch_j. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii48 : ∀a2.eq_ascii ch_k a2 = eq_ascii a2 ch_k. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii49 : ∀a2.eq_ascii ch_l a2 = eq_ascii a2 ch_l. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii50 : ∀a2.eq_ascii ch_m a2 = eq_ascii a2 ch_m. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii51 : ∀a2.eq_ascii ch_n a2 = eq_ascii a2 ch_n. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii52 : ∀a2.eq_ascii ch_o a2 = eq_ascii a2 ch_o. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii53 : ∀a2.eq_ascii ch_p a2 = eq_ascii a2 ch_p. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii54 : ∀a2.eq_ascii ch_q a2 = eq_ascii a2 ch_q. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii55 : ∀a2.eq_ascii ch_r a2 = eq_ascii a2 ch_r. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii56 : ∀a2.eq_ascii ch_s a2 = eq_ascii a2 ch_s. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii57 : ∀a2.eq_ascii ch_t a2 = eq_ascii a2 ch_t. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii58 : ∀a2.eq_ascii ch_u a2 = eq_ascii a2 ch_u. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii59 : ∀a2.eq_ascii ch_v a2 = eq_ascii a2 ch_v. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii60 : ∀a2.eq_ascii ch_w a2 = eq_ascii a2 ch_w. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii61 : ∀a2.eq_ascii ch_x a2 = eq_ascii a2 ch_x. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii62 : ∀a2.eq_ascii ch_y a2 = eq_ascii a2 ch_y. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+nlemma symmetric_eqascii63 : ∀a2.eq_ascii ch_z a2 = eq_ascii a2 ch_z. #a2; ncases a2; nnormalize; napply refl_eq.nqed.
+
+nlemma symmetric_eqascii : symmetricT ascii bool eq_ascii.
+ #a1; ncases a1;
+ ##[ ##1: napply symmetric_eqascii1 ##| ##2: napply symmetric_eqascii2
+ ##| ##3: napply symmetric_eqascii3 ##| ##4: napply symmetric_eqascii4
+ ##| ##5: napply symmetric_eqascii5 ##| ##6: napply symmetric_eqascii6
+ ##| ##7: napply symmetric_eqascii7 ##| ##8: napply symmetric_eqascii8
+ ##| ##9: napply symmetric_eqascii9 ##| ##10: napply symmetric_eqascii10
+ ##| ##11: napply symmetric_eqascii11 ##| ##12: napply symmetric_eqascii12
+ ##| ##13: napply symmetric_eqascii13 ##| ##14: napply symmetric_eqascii14
+ ##| ##15: napply symmetric_eqascii15 ##| ##16: napply symmetric_eqascii16
+ ##| ##17: napply symmetric_eqascii17 ##| ##18: napply symmetric_eqascii18
+ ##| ##19: napply symmetric_eqascii19 ##| ##20: napply symmetric_eqascii20
+ ##| ##21: napply symmetric_eqascii21 ##| ##22: napply symmetric_eqascii22
+ ##| ##23: napply symmetric_eqascii23 ##| ##24: napply symmetric_eqascii24
+ ##| ##25: napply symmetric_eqascii25 ##| ##26: napply symmetric_eqascii26
+ ##| ##27: napply symmetric_eqascii27 ##| ##28: napply symmetric_eqascii28
+ ##| ##29: napply symmetric_eqascii29 ##| ##30: napply symmetric_eqascii30
+ ##| ##31: napply symmetric_eqascii31 ##| ##32: napply symmetric_eqascii32
+ ##| ##33: napply symmetric_eqascii33 ##| ##34: napply symmetric_eqascii34
+ ##| ##35: napply symmetric_eqascii35 ##| ##36: napply symmetric_eqascii36
+ ##| ##37: napply symmetric_eqascii37 ##| ##38: napply symmetric_eqascii38
+ ##| ##39: napply symmetric_eqascii39 ##| ##40: napply symmetric_eqascii40
+ ##| ##41: napply symmetric_eqascii41 ##| ##42: napply symmetric_eqascii42
+ ##| ##43: napply symmetric_eqascii43 ##| ##44: napply symmetric_eqascii44
+ ##| ##45: napply symmetric_eqascii45 ##| ##46: napply symmetric_eqascii46
+ ##| ##47: napply symmetric_eqascii47 ##| ##48: napply symmetric_eqascii48
+ ##| ##49: napply symmetric_eqascii49 ##| ##50: napply symmetric_eqascii50
+ ##| ##51: napply symmetric_eqascii51 ##| ##52: napply symmetric_eqascii52
+ ##| ##53: napply symmetric_eqascii53 ##| ##54: napply symmetric_eqascii54
+ ##| ##55: napply symmetric_eqascii55 ##| ##56: napply symmetric_eqascii56
+ ##| ##57: napply symmetric_eqascii57 ##| ##58: napply symmetric_eqascii58
+ ##| ##59: napply symmetric_eqascii59 ##| ##60: napply symmetric_eqascii60
+ ##| ##61: napply symmetric_eqascii61 ##| ##62: napply symmetric_eqascii62
+ ##| ##63: napply symmetric_eqascii63 ##]
+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_eq : ∀c1,c2.eq_ascii c1 c2 = true → c1 = c2.
+ #c1; ncases c1;
+ ##[ ##1: napply eqascii_to_eq1 ##| ##2: napply eqascii_to_eq2
+ ##| ##3: napply eqascii_to_eq3 ##| ##4: napply eqascii_to_eq4
+ ##| ##5: napply eqascii_to_eq5 ##| ##6: napply eqascii_to_eq6
+ ##| ##7: napply eqascii_to_eq7 ##| ##8: napply eqascii_to_eq8
+ ##| ##9: napply eqascii_to_eq9 ##| ##10: napply eqascii_to_eq10
+ ##| ##11: napply eqascii_to_eq11 ##| ##12: napply eqascii_to_eq12
+ ##| ##13: napply eqascii_to_eq13 ##| ##14: napply eqascii_to_eq14
+ ##| ##15: napply eqascii_to_eq15 ##| ##16: napply eqascii_to_eq16
+ ##| ##17: napply eqascii_to_eq17 ##| ##18: napply eqascii_to_eq18
+ ##| ##19: napply eqascii_to_eq19 ##| ##20: napply eqascii_to_eq20
+ ##| ##21: napply eqascii_to_eq21 ##| ##22: napply eqascii_to_eq22
+ ##| ##23: napply eqascii_to_eq23 ##| ##24: napply eqascii_to_eq24
+ ##| ##25: napply eqascii_to_eq25 ##| ##26: napply eqascii_to_eq26
+ ##| ##27: napply eqascii_to_eq27 ##| ##28: napply eqascii_to_eq28
+ ##| ##29: napply eqascii_to_eq29 ##| ##30: napply eqascii_to_eq30
+ ##| ##31: napply eqascii_to_eq31 ##| ##32: napply eqascii_to_eq32
+ ##| ##33: napply eqascii_to_eq33 ##| ##34: napply eqascii_to_eq34
+ ##| ##35: napply eqascii_to_eq35 ##| ##36: napply eqascii_to_eq36
+ ##| ##37: napply eqascii_to_eq37 ##| ##38: napply eqascii_to_eq38
+ ##| ##39: napply eqascii_to_eq39 ##| ##40: napply eqascii_to_eq40
+ ##| ##41: napply eqascii_to_eq41 ##| ##42: napply eqascii_to_eq42
+ ##| ##43: napply eqascii_to_eq43 ##| ##44: napply eqascii_to_eq44
+ ##| ##45: napply eqascii_to_eq45 ##| ##46: napply eqascii_to_eq46
+ ##| ##47: napply eqascii_to_eq47 ##| ##48: napply eqascii_to_eq48
+ ##| ##49: napply eqascii_to_eq49 ##| ##50: napply eqascii_to_eq50
+ ##| ##51: napply eqascii_to_eq51 ##| ##52: napply eqascii_to_eq52
+ ##| ##53: napply eqascii_to_eq53 ##| ##54: napply eqascii_to_eq54
+ ##| ##55: napply eqascii_to_eq55 ##| ##56: napply eqascii_to_eq56
+ ##| ##57: napply eqascii_to_eq57 ##| ##58: napply eqascii_to_eq58
+ ##| ##59: napply eqascii_to_eq59 ##| ##60: napply eqascii_to_eq60
+ ##| ##61: napply eqascii_to_eq61 ##| ##62: napply eqascii_to_eq62
+ ##| ##63: napply eqascii_to_eq63 ##]
+nqed.
+
+nlemma eq_to_eqascii1 : ∀a2.ch_0 = a2 → eq_ascii ch_0 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii2 : ∀a2.ch_1 = a2 → eq_ascii ch_1 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii3 : ∀a2.ch_2 = a2 → eq_ascii ch_2 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii4 : ∀a2.ch_3 = a2 → eq_ascii ch_3 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii5 : ∀a2.ch_4 = a2 → eq_ascii ch_4 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii6 : ∀a2.ch_5 = a2 → eq_ascii ch_5 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii7 : ∀a2.ch_6 = a2 → eq_ascii ch_6 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii8 : ∀a2.ch_7 = a2 → eq_ascii ch_7 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii9 : ∀a2.ch_8 = a2 → eq_ascii ch_8 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii10 : ∀a2.ch_9 = a2 → eq_ascii ch_9 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii11 : ∀a2.ch__ = a2 → eq_ascii ch__ a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii12 : ∀a2.ch_A = a2 → eq_ascii ch_A a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii13 : ∀a2.ch_B = a2 → eq_ascii ch_B a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii14 : ∀a2.ch_C = a2 → eq_ascii ch_C a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii15 : ∀a2.ch_D = a2 → eq_ascii ch_D a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii16 : ∀a2.ch_E = a2 → eq_ascii ch_E a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii17 : ∀a2.ch_F = a2 → eq_ascii ch_F a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii18 : ∀a2.ch_G = a2 → eq_ascii ch_G a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii19 : ∀a2.ch_H = a2 → eq_ascii ch_H a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii20 : ∀a2.ch_I = a2 → eq_ascii ch_I a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii21 : ∀a2.ch_J = a2 → eq_ascii ch_J a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii22 : ∀a2.ch_K = a2 → eq_ascii ch_K a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii23 : ∀a2.ch_L = a2 → eq_ascii ch_L a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii24 : ∀a2.ch_M = a2 → eq_ascii ch_M a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii25 : ∀a2.ch_N = a2 → eq_ascii ch_N a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii26 : ∀a2.ch_O = a2 → eq_ascii ch_O a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii27 : ∀a2.ch_P = a2 → eq_ascii ch_P a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii28 : ∀a2.ch_Q = a2 → eq_ascii ch_Q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii29 : ∀a2.ch_R = a2 → eq_ascii ch_R a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii30 : ∀a2.ch_S = a2 → eq_ascii ch_S a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii31 : ∀a2.ch_T = a2 → eq_ascii ch_T a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii32 : ∀a2.ch_U = a2 → eq_ascii ch_U a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii33 : ∀a2.ch_V = a2 → eq_ascii ch_V a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii34 : ∀a2.ch_W = a2 → eq_ascii ch_W a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii35 : ∀a2.ch_X = a2 → eq_ascii ch_X a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii36 : ∀a2.ch_Y = a2 → eq_ascii ch_Y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii37 : ∀a2.ch_Z = a2 → eq_ascii ch_Z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii38 : ∀a2.ch_a = a2 → eq_ascii ch_a a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii39 : ∀a2.ch_b = a2 → eq_ascii ch_b a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii40 : ∀a2.ch_c = a2 → eq_ascii ch_c a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii41 : ∀a2.ch_d = a2 → eq_ascii ch_d a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii42 : ∀a2.ch_e = a2 → eq_ascii ch_e a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii43 : ∀a2.ch_f = a2 → eq_ascii ch_f a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii44 : ∀a2.ch_g = a2 → eq_ascii ch_g a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii45 : ∀a2.ch_h = a2 → eq_ascii ch_h a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii46 : ∀a2.ch_i = a2 → eq_ascii ch_i a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii47 : ∀a2.ch_j = a2 → eq_ascii ch_j a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii48 : ∀a2.ch_k = a2 → eq_ascii ch_k a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii49 : ∀a2.ch_l = a2 → eq_ascii ch_l a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii50 : ∀a2.ch_m = a2 → eq_ascii ch_m a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii51 : ∀a2.ch_n = a2 → eq_ascii ch_n a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii52 : ∀a2.ch_o = a2 → eq_ascii ch_o a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii53 : ∀a2.ch_p = a2 → eq_ascii ch_p a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii54 : ∀a2.ch_q = a2 → eq_ascii ch_q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii55 : ∀a2.ch_r = a2 → eq_ascii ch_r a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii56 : ∀a2.ch_s = a2 → eq_ascii ch_s a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii57 : ∀a2.ch_t = a2 → eq_ascii ch_t a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii58 : ∀a2.ch_u = a2 → eq_ascii ch_u a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii59 : ∀a2.ch_v = a2 → eq_ascii ch_v a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii60 : ∀a2.ch_w = a2 → eq_ascii ch_w a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii61 : ∀a2.ch_x = a2 → eq_ascii ch_x a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii62 : ∀a2.ch_y = a2 → eq_ascii ch_y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+nlemma eq_to_eqascii63 : ∀a2.ch_z = a2 → eq_ascii ch_z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: napply (ascii_destruct … H) ##] nqed.
+
+nlemma eq_to_eqascii : ∀c1,c2.c1 = c2 → eq_ascii c1 c2 = true.
+ #c1; ncases c1;
+ ##[ ##1: napply eq_to_eqascii1 ##| ##2: napply eq_to_eqascii2
+ ##| ##3: napply eq_to_eqascii3 ##| ##4: napply eq_to_eqascii4
+ ##| ##5: napply eq_to_eqascii5 ##| ##6: napply eq_to_eqascii6
+ ##| ##7: napply eq_to_eqascii7 ##| ##8: napply eq_to_eqascii8
+ ##| ##9: napply eq_to_eqascii9 ##| ##10: napply eq_to_eqascii10
+ ##| ##11: napply eq_to_eqascii11 ##| ##12: napply eq_to_eqascii12
+ ##| ##13: napply eq_to_eqascii13 ##| ##14: napply eq_to_eqascii14
+ ##| ##15: napply eq_to_eqascii15 ##| ##16: napply eq_to_eqascii16
+ ##| ##17: napply eq_to_eqascii17 ##| ##18: napply eq_to_eqascii18
+ ##| ##19: napply eq_to_eqascii19 ##| ##20: napply eq_to_eqascii20
+ ##| ##21: napply eq_to_eqascii21 ##| ##22: napply eq_to_eqascii22
+ ##| ##23: napply eq_to_eqascii23 ##| ##24: napply eq_to_eqascii24
+ ##| ##25: napply eq_to_eqascii25 ##| ##26: napply eq_to_eqascii26
+ ##| ##27: napply eq_to_eqascii27 ##| ##28: napply eq_to_eqascii28
+ ##| ##29: napply eq_to_eqascii29 ##| ##30: napply eq_to_eqascii30
+ ##| ##31: napply eq_to_eqascii31 ##| ##32: napply eq_to_eqascii32
+ ##| ##33: napply eq_to_eqascii33 ##| ##34: napply eq_to_eqascii34
+ ##| ##35: napply eq_to_eqascii35 ##| ##36: napply eq_to_eqascii36
+ ##| ##37: napply eq_to_eqascii37 ##| ##38: napply eq_to_eqascii38
+ ##| ##39: napply eq_to_eqascii39 ##| ##40: napply eq_to_eqascii40
+ ##| ##41: napply eq_to_eqascii41 ##| ##42: napply eq_to_eqascii42
+ ##| ##43: napply eq_to_eqascii43 ##| ##44: napply eq_to_eqascii44
+ ##| ##45: napply eq_to_eqascii45 ##| ##46: napply eq_to_eqascii46
+ ##| ##47: napply eq_to_eqascii47 ##| ##48: napply eq_to_eqascii48
+ ##| ##49: napply eq_to_eqascii49 ##| ##50: napply eq_to_eqascii50
+ ##| ##51: napply eq_to_eqascii51 ##| ##52: napply eq_to_eqascii52
+ ##| ##53: napply eq_to_eqascii53 ##| ##54: napply eq_to_eqascii54
+ ##| ##55: napply eq_to_eqascii55 ##| ##56: napply eq_to_eqascii56
+ ##| ##57: napply eq_to_eqascii57 ##| ##58: napply eq_to_eqascii58
+ ##| ##59: napply eq_to_eqascii59 ##| ##60: napply eq_to_eqascii60
+ ##| ##61: napply eq_to_eqascii61 ##| ##62: napply eq_to_eqascii62
+ ##| ##63: napply eq_to_eqascii63 ##]
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/theory.ma".
+
+(* *************** *)
+(* LISTE GENERICHE *)
+(* *************** *)
+
+ninductive list (A:Type) : Type ≝
+ nil: list A
+| cons: A → list A → list A.
+
+nlet rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47
+ for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47
+ for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+(* ************** *)
+(* NON-EMPTY LIST *)
+(* ************** *)
+
+(* lista non vuota *)
+ninductive ne_list (A:Type) : Type ≝
+ | ne_nil: A → ne_list A
+ | ne_cons: A → ne_list A → ne_list A.
+
+(* append *)
+nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
+ match l1 with
+ [ ne_nil hd ⇒ ne_cons A hd l2
+ | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
+
+notation "hvbox(hd break §§ tl)"
+ right associative with precedence 46
+ for @{'ne_cons $hd $tl}.
+
+(* \laquo \raquo *)
+notation "« list0 x sep ; break £ y break »"
+ non associative with precedence 90
+ for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
+
+notation "hvbox(l1 break & l2)"
+ right associative with precedence 47
+ for @{'ne_append $l1 $l2 }.
+
+interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
+interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
+interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/list.ma".
+
+(* *************** *)
+(* LISTE GENERICHE *)
+(* *************** *)
+
+nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+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 ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+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 ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
+ #T; #l;
+ nelim l;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #x; #y; #H;
+ nrewrite > H;
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma associative_list : ∀T.associative (list T) (append T).
+ #T; #x; #y; #z;
+ nelim x;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #a; #b; #H;
+ nrewrite > H;
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
+ #T; #l1; #l2; #a;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
+ #T; #a; #l; #l1;
+ nrewrite > (associative_list T l [a] l1);
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+(* ************** *)
+(* NON-EMPTY LIST *)
+(* ************** *)
+
+nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
+ #T; #x1; #x2; #H;
+ nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+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 ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+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 ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma associative_nelist : ∀T.associative (ne_list T) (ne_append T).
+ #T; #x; #y; #z;
+ nelim x;
+ nnormalize;
+ ##[ ##1: #hh; napply refl_eq
+ ##| ##2: #hh; #tt; #H;
+ nrewrite > H;
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma necons_append_commute : ∀T:Type.∀l1,l2:ne_list T.∀a:T.(a §§ (l1 & l2)) = ((a §§ l1) & l2).
+ #T; #l1; #l2; #a;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma append_necons_commute : ∀T:Type.∀a:T.∀l,l1:ne_list T.(l & (a §§ l1)) = (l & «£a») & l1.
+ #T; #a; #l; #l1;
+ nrewrite > (associative_nelist T l «£a» l1);
+ nnormalize;
+ napply refl_eq.
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ******** *)
+(* NATURALI *)
+(* ******** *)
+
+inductive nat : Type ≝
+ O : nat
+| S : nat → nat.
+
+interpretation "Natural numbers" 'N = nat.
+
+default "natural numbers" cic:/matita/common/nat/nat.ind.
+
+alias num (instance 0) = "natural number".
+
+nlet rec eq_nat (n1,n2:nat) on n1 ≝
+ match n1 with
+ [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
+ | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
+ ].
+
+nlet rec le_nat n m ≝
+ match n with
+ [ O ⇒ true
+ | (S p) ⇒ match m with
+ [ O ⇒ false | (S q) ⇒ le_nat p q ]
+ ].
+
+nlet rec plus (n1,n2:nat) on n1 ≝
+ match n1 with
+ [ O ⇒ n2
+ | (S n1') ⇒ S (plus n1' n2) ].
+
+interpretation "natural plus" 'plus x y = (plus x y).
+
+nlet rec times (n1,n2:nat) on n1 ≝
+ match n1 with
+ [ O ⇒ O
+ | (S n1') ⇒ n2 + (times n1' n2) ].
+
+interpretation "natural times" 'times x y = (times x y).
+
+nlet rec minus n m ≝
+ match n with
+ [ O ⇒ O
+ | (S p) ⇒
+ match m with
+ [O ⇒ (S p)
+ | (S q) ⇒ minus p q ]].
+
+interpretation "natural minus" 'minus x y = (minus x y).
+
+nlet rec div_aux p m n : nat ≝
+match (le_nat m n) with
+[ true ⇒ O
+| false ⇒
+ match p with
+ [ O ⇒ O
+ | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
+
+ndefinition div : nat → nat → nat ≝
+λn,m.match m with
+ [ O ⇒ S n
+ | (S p) ⇒ div_aux n n p].
+
+interpretation "natural divide" 'divide x y = (div x y).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/nat.ma".
+include "num/bool_lemmas.ma".
+
+(* ******** *)
+(* NATURALI *)
+(* ******** *)
+
+nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
+ #n1; #n2; #H;
+ nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
+ #n; #H;
+ nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
+ #n; #H;
+ nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
+ nnormalize;
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+ nelim n2;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #n3; #H; napply refl_eq
+ ##]
+ ##| ##2: #n2; #H; #n3;
+ nnormalize;
+ ncases n3;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #n4; napply (H n4)
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+ nelim n2;
+ nnormalize;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
+ ##]
+ ##| ##2: #n2; #H; #n3; #H1;
+ ncases n3 in H1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
+ ##| ##2: #n4; #H1;
+ napply (H n4 (nat_destruct_S_S … H1))
+ ##]
+ ##]
+nqed.
+
+nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+ nelim n2;
+ nnormalize;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##2: #n3; #H; #H1; 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)
+ ##| ##2: #n4; #H1;
+ nrewrite > (H n4 H1);
+ napply refl_eq
+ ##]
+ ##]
+nqed.
+
+nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
+ #n1;
+ nelim n1;
+ ##[ ##1: nnormalize; #n2; napply refl_eq
+ ##| ##2: #n; #H; #n2; nrewrite > (H n2);
+ ncases n in H:(%) ⊢ %;
+ ##[ ##1: nnormalize; #H; napply refl_eq
+ ##| ##2: #n3; nnormalize; #H; napply refl_eq
+ ##]
+ ##]
+nqed.
+
+nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
+ #n1;
+ nelim n1;
+ ##[ ##1: nnormalize; #n2; napply refl_eq
+ ##| ##2: #n; #H; #n2;
+ nrewrite > (Sn_p_n_to_S_npn n (S n2));
+ nrewrite > (H n2);
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma Opn_to_n : ∀n.O + n = n.
+ #n; nnormalize; napply refl_eq.
+nqed.
+
+nlemma npO_to_n : ∀n.n + O = n.
+ #n;
+ nelim n;
+ ##[ ##1: nnormalize; napply refl_eq
+ ##| ##2: #n1; #H;
+ nrewrite > (Sn_p_n_to_S_npn n1 O);
+ nrewrite > H;
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma symmetric_plusnat : symmetricT nat nat plus.
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
+ ##| ##2: #n2; #H; #n3;
+ nrewrite > (Sn_p_n_to_S_npn n2 n3);
+ nrewrite > (n_p_Sn_to_S_npn n3 n2);
+ nrewrite > (H n3);
+ napply refl_eq
+ ##]
+nqed.
+num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
+common/nat.ma num/bool.ma
num/word32.ma num/word16.ma
-num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
-common/option.ma num/bool.ma
-num/word16.ma num/byte8.ma
-num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
-num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
test_errori.ma
-common/theory.ma
-num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
-num/quatern.ma num/bool.ma
-common/prod.ma num/bool.ma
-num/byte8.ma num/bitrigesim.ma num/exadecim.ma
-num/bool.ma common/theory.ma
-num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
+common/list_lemmas.ma common/list.ma
num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
-common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
-common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
-num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
num/bitrigesim.ma num/bool.ma
+common/ascii_lemmas1.ma common/ascii.ma
+num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
+common/prod.ma num/bool.ma
+common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
num/bool_lemmas.ma num/bool.ma
+common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
+common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
+num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
+common/theory.ma
+num/quatern.ma num/bool.ma
num/oct.ma num/bool.ma
+num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
+num/byte8.ma num/bitrigesim.ma num/exadecim.ma
+num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
+common/option.ma num/bool.ma
+common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
+num/bool.ma common/theory.ma
+num/word16.ma num/byte8.ma
+common/ascii.ma num/bool.ma
+common/list.ma common/theory.ma
+num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
projects / helm.git / commitdiff