matita/matita/contribs/ng_assembly/emulator/memory/memory_struct_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_struct.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* **************** *)
  27 (* TIPO ARRAY DA 16 *)
  28 (* **************** *)
  29
  30 nlemma ar16_destruct_1 :
  31 ∀T.
  32 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  33 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  34  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  35  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  36  x1 = y1.
  37  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  38  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  39  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  40                 with [ mk_Array16T a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  41  nrewrite < H;
  42  nnormalize;
  43  napply refl_eq.
  44 nqed.
  45
  46 nlemma ar16_destruct_2 :
  47 ∀T.
  48 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  49 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  50  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  51  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  52  x2 = y2.
  53  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  54  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  55  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  56                 with [ mk_Array16T _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  57  nrewrite < H;
  58  nnormalize;
  59  napply refl_eq.
  60 nqed.
  61
  62 nlemma ar16_destruct_3 :
  63 ∀T.
  64 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  65 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  66  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  67  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  68  x3 = y3.
  69  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  70  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  71  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  72                 with [ mk_Array16T _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  73  nrewrite < H;
  74  nnormalize;
  75  napply refl_eq.
  76 nqed.
  77
  78 nlemma ar16_destruct_4 :
  79 ∀T.
  80 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  81 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  82  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  83  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  84  x4 = y4.
  85  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  86  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  87  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  88                 with [ mk_Array16T _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  89  nrewrite < H;
  90  nnormalize;
  91  napply refl_eq.
  92 nqed.
  93
  94 nlemma ar16_destruct_5 :
  95 ∀T.
  96 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  97 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  98  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  99  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 100  x5 = y5.
 101  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 102  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 103  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 104                 with [ mk_Array16T _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
 105  nrewrite < H;
 106  nnormalize;
 107  napply refl_eq.
 108 nqed.
 109
 110 nlemma ar16_destruct_6 :
 111 ∀T.
 112 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 113 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 114  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 115  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 116  x6 = y6.
 117  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 118  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 119  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 120                 with [ mk_Array16T _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
 121  nrewrite < H;
 122  nnormalize;
 123  napply refl_eq.
 124 nqed.
 125
 126 nlemma ar16_destruct_7 :
 127 ∀T.
 128 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 129 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 130  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 131  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 132  x7 = y7.
 133  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 134  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 135  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 136                 with [ mk_Array16T _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
 137  nrewrite < H;
 138  nnormalize;
 139  napply refl_eq.
 140 nqed.
 141
 142 nlemma ar16_destruct_8 :
 143 ∀T.
 144 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 145 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 146  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 147  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 148  x8 = y8.
 149  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 150  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 151  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 152                 with [ mk_Array16T _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
 153  nrewrite < H;
 154  nnormalize;
 155  napply refl_eq.
 156 nqed.
 157
 158 nlemma ar16_destruct_9 :
 159 ∀T.
 160 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 161 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 162  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 163  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 164  x9 = y9.
 165  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 166  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 167  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 168                 with [ mk_Array16T _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
 169  nrewrite < H;
 170  nnormalize;
 171  napply refl_eq.
 172 nqed.
 173
 174 nlemma ar16_destruct_10 :
 175 ∀T.
 176 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 177 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 178  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 179  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 180  x10 = y10.
 181  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 182  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 183  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 184                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
 185  nrewrite < H;
 186  nnormalize;
 187  napply refl_eq.
 188 nqed.
 189
 190 nlemma ar16_destruct_11 :
 191 ∀T.
 192 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 193 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 194  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 195  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 196  x11 = y11.
 197  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 198  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 199  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 200                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
 201  nrewrite < H;
 202  nnormalize;
 203  napply refl_eq.
 204 nqed.
 205
 206 nlemma ar16_destruct_12 :
 207 ∀T.
 208 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 209 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 210  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 211  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 212  x12 = y12.
 213  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 214  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 215  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 216                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
 217  nrewrite < H;
 218  nnormalize;
 219  napply refl_eq.
 220 nqed.
 221
 222 nlemma ar16_destruct_13 :
 223 ∀T.
 224 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 225 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 226  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 227  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 228  x13 = y13.
 229  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 230  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 231  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 232                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
 233  nrewrite < H;
 234  nnormalize;
 235  napply refl_eq.
 236 nqed.
 237
 238 nlemma ar16_destruct_14 :
 239 ∀T.
 240 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 241 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 242  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 243  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 244  x14 = y14.
 245  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 246  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 247  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 248                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
 249  nrewrite < H;
 250  nnormalize;
 251  napply refl_eq.
 252 nqed.
 253
 254 nlemma ar16_destruct_15 :
 255 ∀T.
 256 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 257 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 258  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 259  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 260  x15 = y15.
 261  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 262  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 263  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 264                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
 265  nrewrite < H;
 266  nnormalize;
 267  napply refl_eq.
 268 nqed.
 269
 270 nlemma ar16_destruct_16 :
 271 ∀T.
 272 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 273 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 274  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 275  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 276  x16 = y16.
 277  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 278  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 279  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 280                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
 281  nrewrite < H;
 282  nnormalize;
 283  napply refl_eq.
 284 nqed.
 285
 286 nlemma symmetric_eqar16 :
 287 ∀T.∀f:T → T → bool.
 288  (symmetricT T bool f) →
 289  (symmetricT (Array16T T) bool (eq_ar16 T f)).
 290  #T; #f; #H;
 291  #alu1; ncases alu1;
 292  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 293  #alu2; ncases alu2;
 294  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 295  nchange with (
 296   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 297    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
 298    (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
 299    (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) =
 300   ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
 301    (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8) ⊗
 302    (f y9 x9) ⊗ (f y10 x10) ⊗ (f y11 x11) ⊗ (f y12 x12) ⊗
 303    (f y13 x13) ⊗ (f y14 x14) ⊗ (f y15 x15) ⊗ (f y16 x16)));
 304  nrewrite > (H x1 y1);
 305  nrewrite > (H x2 y2);
 306  nrewrite > (H x3 y3);
 307  nrewrite > (H x4 y4);
 308  nrewrite > (H x5 y5);
 309  nrewrite > (H x6 y6);
 310  nrewrite > (H x7 y7);
 311  nrewrite > (H x8 y8);
 312  nrewrite > (H x9 y9);
 313  nrewrite > (H x10 y10);
 314  nrewrite > (H x11 y11);
 315  nrewrite > (H x12 y12);
 316  nrewrite > (H x13 y13);
 317  nrewrite > (H x14 y14);
 318  nrewrite > (H x15 y15);
 319  nrewrite > (H x16 y16);
 320  napply refl_eq.
 321 nqed.
 322
 323 nlemma eqar16_to_eq :
 324 ∀T.∀f:T → T → bool.
 325  (∀x,y.(f x y = true) → (x = y)) →
 326  (∀a1,a2:Array16T T.(eq_ar16 T f a1 a2 = true) → (a1 = a2)).
 327  #T; #f; #H;
 328  #alu1; ncases alu1;
 329  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 330  #alu2; ncases alu2;
 331  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
 332  nchange in H1:(%) with (
 333   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 334    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
 335    (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
 336    (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) = true);
 337  nrewrite > (H … (andb_true_true_r … H1));
 338  nletin H2 ≝ (andb_true_true_l … H1);
 339  nrewrite > (H … (andb_true_true_r … H2));
 340  nletin H3 ≝ (andb_true_true_l … H2);
 341  nrewrite > (H … (andb_true_true_r … H3));
 342  nletin H4 ≝ (andb_true_true_l … H3);
 343  nrewrite > (H … (andb_true_true_r … H4));
 344  nletin H5 ≝ (andb_true_true_l … H4);
 345  nrewrite > (H … (andb_true_true_r … H5));
 346  nletin H6 ≝ (andb_true_true_l … H5);
 347  nrewrite > (H … (andb_true_true_r … H6));
 348  nletin H7 ≝ (andb_true_true_l … H6);
 349  nrewrite > (H … (andb_true_true_r … H7));
 350  nletin H8 ≝ (andb_true_true_l … H7);
 351  nrewrite > (H … (andb_true_true_r … H8));
 352  nletin H9 ≝ (andb_true_true_l … H8);
 353  nrewrite > (H … (andb_true_true_r … H9));
 354  nletin H10 ≝ (andb_true_true_l … H9);
 355  nrewrite > (H … (andb_true_true_r … H10));
 356  nletin H11 ≝ (andb_true_true_l … H10);
 357  nrewrite > (H … (andb_true_true_r … H11));
 358  nletin H12 ≝ (andb_true_true_l … H11);
 359  nrewrite > (H … (andb_true_true_r … H12));
 360  nletin H13 ≝ (andb_true_true_l … H12);
 361  nrewrite > (H … (andb_true_true_r … H13));
 362  nletin H14 ≝ (andb_true_true_l … H13);
 363  nrewrite > (H … (andb_true_true_r … H14));
 364  nletin H15 ≝ (andb_true_true_l … H14);
 365  nrewrite > (H … (andb_true_true_r … H15));
 366  nrewrite > (H … (andb_true_true_l … H15));
 367  napply refl_eq.
 368 nqed.
 369
 370 nlemma eq_to_eqar16 :
 371 ∀T.∀f:T → T → bool.
 372  (∀x,y.(x = y) → (f x y = true)) →
 373  (∀a1,a2:Array16T T.(a1 = a2) → (eq_ar16 T f a1 a2 = true)).
 374  #T; #f; #H;
 375  #alu1; ncases alu1;
 376  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 377  #alu2; ncases alu2;
 378  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
 379  nrewrite > (ar16_destruct_1 … H1);
 380  nrewrite > (ar16_destruct_2 … H1);
 381  nrewrite > (ar16_destruct_3 … H1);
 382  nrewrite > (ar16_destruct_4 … H1);
 383  nrewrite > (ar16_destruct_5 … H1);
 384  nrewrite > (ar16_destruct_6 … H1);
 385  nrewrite > (ar16_destruct_7 … H1);
 386  nrewrite > (ar16_destruct_8 … H1);
 387  nrewrite > (ar16_destruct_9 … H1);
 388  nrewrite > (ar16_destruct_10 … H1);
 389  nrewrite > (ar16_destruct_11 … H1);
 390  nrewrite > (ar16_destruct_12 … H1);
 391  nrewrite > (ar16_destruct_13 … H1);
 392  nrewrite > (ar16_destruct_14 … H1);
 393  nrewrite > (ar16_destruct_15 … H1);
 394  nrewrite > (ar16_destruct_16 … H1);
 395  nchange with (
 396   ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
 397    (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8) ⊗
 398    (f y9 y9) ⊗ (f y10 y10) ⊗ (f y11 y11) ⊗ (f y12 y12) ⊗
 399    (f y13 y13) ⊗ (f y14 y14) ⊗ (f y15 y15) ⊗ (f y16 y16)) = true);
 400  nrewrite > (H … (refl_eq …));
 401  nrewrite > (H … (refl_eq …));
 402  nrewrite > (H … (refl_eq …));
 403  nrewrite > (H … (refl_eq …));
 404  nrewrite > (H … (refl_eq …));
 405  nrewrite > (H … (refl_eq …));
 406  nrewrite > (H … (refl_eq …));
 407  nrewrite > (H … (refl_eq …));
 408  nrewrite > (H … (refl_eq …));
 409  nrewrite > (H … (refl_eq …));
 410  nrewrite > (H … (refl_eq …));
 411  nrewrite > (H … (refl_eq …));
 412  nrewrite > (H … (refl_eq …));
 413  nrewrite > (H … (refl_eq …));
 414  nrewrite > (H … (refl_eq …));
 415  nrewrite > (H … (refl_eq …));
 416  napply refl_eq.
 417 nqed.
 418
 419 nlemma decidable_ar16_aux1 :
 420 ∀T.
 421 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 422 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 423  (x1 ≠ y1) →
 424  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 425  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 426  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 427  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 428  nnormalize; #H; #H1;
 429  napply (H (ar16_destruct_1 … H1)).
 430 nqed.
 431
 432 nlemma decidable_ar16_aux2 :
 433 ∀T.
 434 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 435 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 436  (x2 ≠ y2) →
 437  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 438  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 439  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 440  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 441  nnormalize; #H; #H1;
 442  napply (H (ar16_destruct_2 … H1)).
 443 nqed.
 444
 445 nlemma decidable_ar16_aux3 :
 446 ∀T.
 447 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 448 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 449  (x3 ≠ y3) →
 450  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 451  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 452  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 453  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 454  nnormalize; #H; #H1;
 455  napply (H (ar16_destruct_3 … H1)).
 456 nqed.
 457
 458 nlemma decidable_ar16_aux4 :
 459 ∀T.
 460 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 461 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 462  (x4 ≠ y4) →
 463  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 464  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 465  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 466  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 467  nnormalize; #H; #H1;
 468  napply (H (ar16_destruct_4 … H1)).
 469 nqed.
 470
 471 nlemma decidable_ar16_aux5 :
 472 ∀T.
 473 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 474 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 475  (x5 ≠ y5) →
 476  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 477  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 478  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 479  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 480  nnormalize; #H; #H1;
 481  napply (H (ar16_destruct_5 … H1)).
 482 nqed.
 483
 484 nlemma decidable_ar16_aux6 :
 485 ∀T.
 486 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 487 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 488  (x6 ≠ y6) →
 489  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 490  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 491  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 492  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 493  nnormalize; #H; #H1;
 494  napply (H (ar16_destruct_6 … H1)).
 495 nqed.
 496
 497 nlemma decidable_ar16_aux7 :
 498 ∀T.
 499 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 500 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 501  (x7 ≠ y7) →
 502  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 503  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 504  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 505  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 506  nnormalize; #H; #H1;
 507  napply (H (ar16_destruct_7 … H1)).
 508 nqed.
 509
 510 nlemma decidable_ar16_aux8 :
 511 ∀T.
 512 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 513 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 514  (x8 ≠ y8) →
 515  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 516  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 517  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 518  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 519  nnormalize; #H; #H1;
 520  napply (H (ar16_destruct_8 … H1)).
 521 nqed.
 522
 523 nlemma decidable_ar16_aux9 :
 524 ∀T.
 525 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 526 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 527  (x9 ≠ y9) →
 528  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 529  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 530  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 531  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 532  nnormalize; #H; #H1;
 533  napply (H (ar16_destruct_9 … H1)).
 534 nqed.
 535
 536 nlemma decidable_ar16_aux10 :
 537 ∀T.
 538 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 539 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 540  (x10 ≠ y10) →
 541  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 542  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 543  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 544  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 545  nnormalize; #H; #H1;
 546  napply (H (ar16_destruct_10 … H1)).
 547 nqed.
 548
 549 nlemma decidable_ar16_aux11 :
 550 ∀T.
 551 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 552 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 553  (x11 ≠ y11) →
 554  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 555  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 556  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 557  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 558  nnormalize; #H; #H1;
 559  napply (H (ar16_destruct_11 … H1)).
 560 nqed.
 561
 562 nlemma decidable_ar16_aux12 :
 563 ∀T.
 564 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 565 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 566  (x12 ≠ y12) →
 567  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 568  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 569  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 570  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 571  nnormalize; #H; #H1;
 572  napply (H (ar16_destruct_12 … H1)).
 573 nqed.
 574
 575 nlemma decidable_ar16_aux13 :
 576 ∀T.
 577 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 578 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 579  (x13 ≠ y13) →
 580  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 581  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 582  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 583  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 584  nnormalize; #H; #H1;
 585  napply (H (ar16_destruct_13 … H1)).
 586 nqed.
 587
 588 nlemma decidable_ar16_aux14 :
 589 ∀T.
 590 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 591 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 592  (x14 ≠ y14) →
 593  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 594  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 595  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 596  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 597  nnormalize; #H; #H1;
 598  napply (H (ar16_destruct_14 … H1)).
 599 nqed.
 600
 601 nlemma decidable_ar16_aux15 :
 602 ∀T.
 603 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 604 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 605  (x15 ≠ y15) →
 606  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 607  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 608  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 609  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 610  nnormalize; #H; #H1;
 611  napply (H (ar16_destruct_15 … H1)).
 612 nqed.
 613
 614 nlemma decidable_ar16_aux16 :
 615 ∀T.
 616 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 617 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 618  (x16 ≠ y16) →
 619  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 620  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 621  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 622  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 623  nnormalize; #H; #H1;
 624  napply (H (ar16_destruct_16 … H1)).
 625 nqed.
 626
 627 nlemma decidable_ar16 :
 628 ∀T.(∀x,y:T.decidable (x = y)) →
 629    (∀a1,a2:Array16T T.decidable (a1 = a2)).
 630  #T; #H;
 631  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 632  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 633  nnormalize;
 634  napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
 635  ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar16_aux1 T … H1))
 636  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
 637   ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar16_aux2 T … H2))
 638   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
 639    ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar16_aux3 T … H3))
 640    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
 641     ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar16_aux4 T … H4))
 642     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
 643      ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar16_aux5 T … H5))
 644      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
 645       ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar16_aux6 T … H6))
 646       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
 647        ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar16_aux7 T … H7))
 648        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
 649         ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar16_aux8 T … H8))
 650         ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (H x9 y9) …);
 651          ##[ ##2: #H9; napply (or2_intro2 … (decidable_ar16_aux9 T … H9))
 652          ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (H x10 y10) …);
 653           ##[ ##2: #H10; napply (or2_intro2 … (decidable_ar16_aux10 T … H10))
 654           ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (H x11 y11) …);
 655            ##[ ##2: #H11; napply (or2_intro2 … (decidable_ar16_aux11 T … H11))
 656            ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (H x12 y12) …);
 657             ##[ ##2: #H12; napply (or2_intro2 … (decidable_ar16_aux12 T … H12))
 658             ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (H x13 y13) …);
 659              ##[ ##2: #H13; napply (or2_intro2 … (decidable_ar16_aux13 T … H13))
 660              ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (H x14 y14) …);
 661               ##[ ##2: #H14; napply (or2_intro2 … (decidable_ar16_aux14 T … H14))
 662               ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (H x15 y15) …);
 663                ##[ ##2: #H15; napply (or2_intro2 … (decidable_ar16_aux15 T … H15))
 664                ##| ##1: #H15; napply (or2_elim (? = ?) (? ≠ ?) ? (H x16 y16) …);
 665                 ##[ ##2: #H16; napply (or2_intro2 … (decidable_ar16_aux16 T … H16))
 666                 ##| ##1: #H16; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
 667                       nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
 668                       nrewrite > H9; nrewrite > H10; nrewrite > H11; nrewrite > H12;
 669                       nrewrite > H13; nrewrite > H14; nrewrite > H15; nrewrite > H16;
 670                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 671                 ##]
 672                ##]
 673               ##]
 674              ##]
 675             ##]
 676            ##]
 677           ##]
 678          ##]
 679         ##]
 680        ##]
 681       ##]
 682      ##]
 683     ##]
 684    ##]
 685   ##]
 686  ##]
 687 nqed.
 688
 689 (* *************** *)
 690 (* TIPO ARRAY DA 8 *)
 691 (* *************** *)
 692
 693 nlemma ar8_destruct_1 :
 694 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 695  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 696  x1 = y1.
 697  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 698  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 699                 with [ mk_Array8T a _ _ _ _ _ _ _ ⇒ x1 = a ]);
 700  nrewrite < H;
 701  nnormalize;
 702  napply refl_eq.
 703 nqed.
 704
 705 nlemma ar8_destruct_2 :
 706 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 707  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 708  x2 = y2.
 709  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 710  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 711                 with [ mk_Array8T _ a _ _ _ _ _ _ ⇒ x2 = a ]);
 712  nrewrite < H;
 713  nnormalize;
 714  napply refl_eq.
 715 nqed.
 716
 717 nlemma ar8_destruct_3 :
 718 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 719  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 720  x3 = y3.
 721  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 722  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 723                 with [ mk_Array8T _ _ a _ _ _ _ _ ⇒ x3 = a ]);
 724  nrewrite < H;
 725  nnormalize;
 726  napply refl_eq.
 727 nqed.
 728
 729 nlemma ar8_destruct_4 :
 730 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 731  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 732  x4 = y4.
 733  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 734  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 735                 with [ mk_Array8T _ _ _ a _ _ _ _ ⇒ x4 = a ]);
 736  nrewrite < H;
 737  nnormalize;
 738  napply refl_eq.
 739 nqed.
 740
 741 nlemma ar8_destruct_5 :
 742 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 743  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 744  x5 = y5.
 745  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 746  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 747                 with [ mk_Array8T _ _ _ _ a _ _ _ ⇒ x5 = a ]);
 748  nrewrite < H;
 749  nnormalize;
 750  napply refl_eq.
 751 nqed.
 752
 753 nlemma ar8_destruct_6 :
 754 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 755  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 756  x6 = y6.
 757  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 758  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 759                 with [ mk_Array8T _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 760  nrewrite < H;
 761  nnormalize;
 762  napply refl_eq.
 763 nqed.
 764
 765 nlemma ar8_destruct_7 :
 766 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 767  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 768  x7 = y7.
 769  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 770  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 771                 with [ mk_Array8T _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 772  nrewrite < H;
 773  nnormalize;
 774  napply refl_eq.
 775 nqed.
 776
 777 nlemma ar8_destruct_8 :
 778 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 779  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 780  x8 = y8.
 781  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 782  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 783                 with [ mk_Array8T _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 784  nrewrite < H;
 785  nnormalize;
 786  napply refl_eq.
 787 nqed.
 788
 789 nlemma symmetric_eqar8 :
 790 ∀T.∀f:T → T → bool.
 791  (symmetricT T bool f) →
 792  (symmetricT (Array8T T) bool (eq_ar8 T f)).
 793  #T; #f; #H;
 794  #alu1; ncases alu1;
 795  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 796  #alu2; ncases alu2;
 797  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 798  nchange with (
 799   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 800    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) =
 801   ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
 802    (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8)));
 803  nrewrite > (H x1 y1);
 804  nrewrite > (H x2 y2);
 805  nrewrite > (H x3 y3);
 806  nrewrite > (H x4 y4);
 807  nrewrite > (H x5 y5);
 808  nrewrite > (H x6 y6);
 809  nrewrite > (H x7 y7);
 810  nrewrite > (H x8 y8);
 811  napply refl_eq.
 812 nqed.
 813
 814 nlemma eqar8_to_eq :
 815 ∀T.∀f:T → T → bool.
 816  (∀x,y.(f x y = true) → (x = y)) →
 817  (∀a1,a2:Array8T T.(eq_ar8 T f a1 a2 = true) → (a1 = a2)).
 818  #T; #f; #H;
 819  #alu1; ncases alu1;
 820  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 821  #alu2; ncases alu2;
 822  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
 823  nchange in H1:(%) with (
 824   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 825    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) = true);
 826  nrewrite > (H … (andb_true_true_r … H1));
 827  nletin H2 ≝ (andb_true_true_l … H1);
 828  nrewrite > (H … (andb_true_true_r … H2));
 829  nletin H3 ≝ (andb_true_true_l … H2);
 830  nrewrite > (H … (andb_true_true_r … H3));
 831  nletin H4 ≝ (andb_true_true_l … H3);
 832  nrewrite > (H … (andb_true_true_r … H4));
 833  nletin H5 ≝ (andb_true_true_l … H4);
 834  nrewrite > (H … (andb_true_true_r … H5));
 835  nletin H6 ≝ (andb_true_true_l … H5);
 836  nrewrite > (H … (andb_true_true_r … H6));
 837  nletin H7 ≝ (andb_true_true_l … H6);
 838  nrewrite > (H … (andb_true_true_r … H7));
 839  nrewrite > (H … (andb_true_true_l … H7));
 840  napply refl_eq.
 841 nqed.
 842
 843 nlemma eq_to_eqar8 :
 844 ∀T.∀f:T → T → bool.
 845  (∀x,y.(x = y) → (f x y = true)) →
 846  (∀a1,a2:Array8T T.(a1 = a2) → (eq_ar8 T f a1 a2 = true)).
 847  #T; #f; #H;
 848  #alu1; ncases alu1;
 849  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 850  #alu2; ncases alu2;
 851  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
 852  nrewrite > (ar8_destruct_1 … H1);
 853  nrewrite > (ar8_destruct_2 … H1);
 854  nrewrite > (ar8_destruct_3 … H1);
 855  nrewrite > (ar8_destruct_4 … H1);
 856  nrewrite > (ar8_destruct_5 … H1);
 857  nrewrite > (ar8_destruct_6 … H1);
 858  nrewrite > (ar8_destruct_7 … H1);
 859  nrewrite > (ar8_destruct_8 … H1);
 860  nchange with (
 861   ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
 862    (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8)) = true);
 863  nrewrite > (H … (refl_eq …));
 864  nrewrite > (H … (refl_eq …));
 865  nrewrite > (H … (refl_eq …));
 866  nrewrite > (H … (refl_eq …));
 867  nrewrite > (H … (refl_eq …));
 868  nrewrite > (H … (refl_eq …));
 869  nrewrite > (H … (refl_eq …));
 870  nrewrite > (H … (refl_eq …));
 871  napply refl_eq.
 872 nqed.
 873
 874 nlemma decidable_ar8_aux1 :
 875 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 876  (x1 ≠ y1) →
 877  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 878  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 879  nnormalize; #H; #H1;
 880  napply (H (ar8_destruct_1 … H1)).
 881 nqed.
 882
 883 nlemma decidable_ar8_aux2 :
 884 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 885  (x2 ≠ y2) →
 886  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 887  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 888  nnormalize; #H; #H1;
 889  napply (H (ar8_destruct_2 … H1)).
 890 nqed.
 891
 892 nlemma decidable_ar8_aux3 :
 893 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 894  (x3 ≠ y3) →
 895  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 896  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 897  nnormalize; #H; #H1;
 898  napply (H (ar8_destruct_3 … H1)).
 899 nqed.
 900
 901 nlemma decidable_ar8_aux4 :
 902 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 903  (x4 ≠ y4) →
 904  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 905  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 906  nnormalize; #H; #H1;
 907  napply (H (ar8_destruct_4 … H1)).
 908 nqed.
 909
 910 nlemma decidable_ar8_aux5 :
 911 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 912  (x5 ≠ y5) →
 913  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 914  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 915  nnormalize; #H; #H1;
 916  napply (H (ar8_destruct_5 … H1)).
 917 nqed.
 918
 919 nlemma decidable_ar8_aux6 :
 920 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 921  (x6 ≠ y6) →
 922  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 923  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 924  nnormalize; #H; #H1;
 925  napply (H (ar8_destruct_6 … H1)).
 926 nqed.
 927
 928 nlemma decidable_ar8_aux7 :
 929 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 930  (x7 ≠ y7) →
 931  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 932  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 933  nnormalize; #H; #H1;
 934  napply (H (ar8_destruct_7 … H1)).
 935 nqed.
 936
 937 nlemma decidable_ar8_aux8 :
 938 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 939  (x8 ≠ y8) →
 940  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 941  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 942  nnormalize; #H; #H1;
 943  napply (H (ar8_destruct_8 … H1)).
 944 nqed.
 945
 946 nlemma decidable_ar8 :
 947 ∀T.(∀x,y:T.decidable (x = y)) →
 948    (∀a1,a2:Array8T T.decidable (a1 = a2)).
 949  #T; #H;
 950  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 951  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 952  nnormalize;
 953  napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
 954  ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar8_aux1 T … H1))
 955  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
 956   ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar8_aux2 T … H2))
 957   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
 958    ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar8_aux3 T … H3))
 959    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
 960     ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar8_aux4 T … H4))
 961     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
 962      ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar8_aux5 T … H5))
 963      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
 964       ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar8_aux6 T … H6))
 965       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
 966        ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar8_aux7 T … H7))
 967        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
 968         ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar8_aux8 T … H8))
 969         ##| ##1: #H8; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
 970                       nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
 971                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 972         ##]
 973        ##]
 974       ##]
 975      ##]
 976     ##]
 977    ##]
 978   ##]
 979  ##]
 980 nqed.