freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / ascii_lemmas3.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma
index de510fe40dd57bc952dcc6cef57baae5ae44c8ba..98dabd50e2a42f900d7fac12d5b8c68dd162fe2f 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma
@@ -29,442 +29,442 @@ include "num/bool_lemmas.ma".
 
 nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x).
  #x; nnormalize; nelim x;
- ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x).
  #x; nnormalize; nelim x;
- ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x).
  #x; nnormalize; nelim x;
- ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x).
  #x; nnormalize; nelim x;
- ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x).
  #x; nnormalize; nelim x;
- ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x).
  #x; nnormalize; nelim x;
- ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x).
  #x; nnormalize; nelim x;
- ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x).
  #x; nnormalize; nelim x;
- ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x).
  #x; nnormalize; nelim x;
- ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x).
  #x; nnormalize; nelim x;
- ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x).
  #x; nnormalize; nelim x;
- ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x).
  #x; nnormalize; nelim x;
- ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x).
  #x; nnormalize; nelim x;
- ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x).
  #x; nnormalize; nelim x;
- ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x).
  #x; nnormalize; nelim x;
- ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x).
  #x; nnormalize; nelim x;
- ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x).
  #x; nnormalize; nelim x;
- ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x).
  #x; nnormalize; nelim x;
- ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x).
  #x; nnormalize; nelim x;
- ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x).
  #x; nnormalize; nelim x;
- ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x).
  #x; nnormalize; nelim x;
- ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x).
  #x; nnormalize; nelim x;
- ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x).
  #x; nnormalize; nelim x;
- ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x).
  #x; nnormalize; nelim x;
- ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x).
  #x; nnormalize; nelim x;
- ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x).
  #x; nnormalize; nelim x;
- ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x).
  #x; nnormalize; nelim x;
- ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x).
  #x; nnormalize; nelim x;
- ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x).
  #x; nnormalize; nelim x;
- ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x).
  #x; nnormalize; nelim x;
- ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x).
  #x; nnormalize; nelim x;
- ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x).
  #x; nnormalize; nelim x;
- ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x).
  #x; nnormalize; nelim x;
- ##[ ##33: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x).
  #x; nnormalize; nelim x;
- ##[ ##34: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x).
  #x; nnormalize; nelim x;
- ##[ ##35: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x).
  #x; nnormalize; nelim x;
- ##[ ##36: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x).
  #x; nnormalize; nelim x;
- ##[ ##37: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x).
  #x; nnormalize; nelim x;
- ##[ ##38: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x).
  #x; nnormalize; nelim x;
- ##[ ##39: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x).
  #x; nnormalize; nelim x;
- ##[ ##40: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x).
  #x; nnormalize; nelim x;
- ##[ ##41: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x).
  #x; nnormalize; nelim x;
- ##[ ##42: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x).
  #x; nnormalize; nelim x;
- ##[ ##43: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x).
  #x; nnormalize; nelim x;
- ##[ ##44: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x).
  #x; nnormalize; nelim x;
- ##[ ##45: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x).
  #x; nnormalize; nelim x;
- ##[ ##46: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x).
  #x; nnormalize; nelim x;
- ##[ ##47: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x).
  #x; nnormalize; nelim x;
- ##[ ##48: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x).
  #x; nnormalize; nelim x;
- ##[ ##49: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x).
  #x; nnormalize; nelim x;
- ##[ ##50: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x).
  #x; nnormalize; nelim x;
- ##[ ##51: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x).
  #x; nnormalize; nelim x;
- ##[ ##52: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x).
  #x; nnormalize; nelim x;
- ##[ ##53: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x).
  #x; nnormalize; nelim x;
- ##[ ##54: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x).
  #x; nnormalize; nelim x;
- ##[ ##55: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x).
  #x; nnormalize; nelim x;
- ##[ ##56: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x).
  #x; nnormalize; nelim x;
- ##[ ##57: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x).
  #x; nnormalize; nelim x;
- ##[ ##58: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x).
  #x; nnormalize; nelim x;
- ##[ ##59: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x).
  #x; nnormalize; nelim x;
- ##[ ##60: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x).
  #x; nnormalize; nelim x;
- ##[ ##61: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x).
  #x; nnormalize; nelim x;
- ##[ ##62: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.
 
 nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x).
  #x; nnormalize; nelim x;
- ##[ ##63: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  ##]
 nqed.