]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct_lemmas.ma
wip ....
[helm.git] / helm / software / 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.