freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / ascii_lemmas1.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
index efab13f9dc46e62f566600069002f2f53488ea53..1c14a97746d61693c6851813143814edde245658 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
@@ -37,434 +37,434 @@ 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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #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
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  ##]
 nqed.