1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "Basic-1/subst0/props.ma".
19 theorem subst0_subst0:
20 \forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0
21 j u2 t1 t2) \to (\forall (u1: T).(\forall (u: T).(\forall (i: nat).((subst0 i
22 u u1 u2) \to (ex2 T (\lambda (t: T).(subst0 j u1 t1 t)) (\lambda (t:
23 T).(subst0 (S (plus i j)) u t t2)))))))))))
25 \lambda (t1: T).(\lambda (t2: T).(\lambda (u2: T).(\lambda (j: nat).(\lambda
26 (H: (subst0 j u2 t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t:
27 T).(\lambda (t0: T).(\lambda (t3: T).(\forall (u1: T).(\forall (u:
28 T).(\forall (i: nat).((subst0 i u u1 t) \to (ex2 T (\lambda (t4: T).(subst0 n
29 u1 t0 t4)) (\lambda (t4: T).(subst0 (S (plus i n)) u t4 t3)))))))))))
30 (\lambda (v: T).(\lambda (i: nat).(\lambda (u1: T).(\lambda (u: T).(\lambda
31 (i0: nat).(\lambda (H0: (subst0 i0 u u1 v)).(eq_ind nat (plus i0 (S i))
32 (\lambda (n: nat).(ex2 T (\lambda (t: T).(subst0 i u1 (TLRef i) t)) (\lambda
33 (t: T).(subst0 n u t (lift (S i) O v))))) (ex_intro2 T (\lambda (t:
34 T).(subst0 i u1 (TLRef i) t)) (\lambda (t: T).(subst0 (plus i0 (S i)) u t
35 (lift (S i) O v))) (lift (S i) O u1) (subst0_lref u1 i) (subst0_lift_ge u1 v
36 u i0 (S i) H0 O (le_O_n i0))) (S (plus i0 i)) (sym_eq nat (S (plus i0 i))
37 (plus i0 (S i)) (plus_n_Sm i0 i))))))))) (\lambda (v: T).(\lambda (u0:
38 T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1
39 u0)).(\lambda (H1: ((\forall (u3: T).(\forall (u: T).(\forall (i0:
40 nat).((subst0 i0 u u3 v) \to (ex2 T (\lambda (t: T).(subst0 i u3 u1 t))
41 (\lambda (t: T).(subst0 (S (plus i0 i)) u t u0))))))))).(\lambda (t:
42 T).(\lambda (k: K).(\lambda (u3: T).(\lambda (u: T).(\lambda (i0:
43 nat).(\lambda (H2: (subst0 i0 u u3 v)).(ex2_ind T (\lambda (t0: T).(subst0 i
44 u3 u1 t0)) (\lambda (t0: T).(subst0 (S (plus i0 i)) u t0 u0)) (ex2 T (\lambda
45 (t0: T).(subst0 i u3 (THead k u1 t) t0)) (\lambda (t0: T).(subst0 (S (plus i0
46 i)) u t0 (THead k u0 t)))) (\lambda (x: T).(\lambda (H3: (subst0 i u3 u1
47 x)).(\lambda (H4: (subst0 (S (plus i0 i)) u x u0)).(ex_intro2 T (\lambda (t0:
48 T).(subst0 i u3 (THead k u1 t) t0)) (\lambda (t0: T).(subst0 (S (plus i0 i))
49 u t0 (THead k u0 t))) (THead k x t) (subst0_fst u3 x u1 i H3 t k) (subst0_fst
50 u u0 x (S (plus i0 i)) H4 t k))))) (H1 u3 u i0 H2)))))))))))))) (\lambda (k:
51 K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i:
52 nat).(\lambda (_: (subst0 (s k i) v t3 t0)).(\lambda (H1: ((\forall (u1:
53 T).(\forall (u: T).(\forall (i0: nat).((subst0 i0 u u1 v) \to (ex2 T (\lambda
54 (t: T).(subst0 (s k i) u1 t3 t)) (\lambda (t: T).(subst0 (S (plus i0 (s k
55 i))) u t t0))))))))).(\lambda (u: T).(\lambda (u1: T).(\lambda (u0:
56 T).(\lambda (i0: nat).(\lambda (H2: (subst0 i0 u0 u1 v)).(ex2_ind T (\lambda
57 (t: T).(subst0 (s k i) u1 t3 t)) (\lambda (t: T).(subst0 (S (plus i0 (s k
58 i))) u0 t t0)) (ex2 T (\lambda (t: T).(subst0 i u1 (THead k u t3) t))
59 (\lambda (t: T).(subst0 (S (plus i0 i)) u0 t (THead k u t0)))) (\lambda (x:
60 T).(\lambda (H3: (subst0 (s k i) u1 t3 x)).(\lambda (H4: (subst0 (S (plus i0
61 (s k i))) u0 x t0)).(let H5 \def (eq_ind_r nat (plus i0 (s k i)) (\lambda (n:
62 nat).(subst0 (S n) u0 x t0)) H4 (s k (plus i0 i)) (s_plus_sym k i0 i)) in
63 (let H6 \def (eq_ind_r nat (S (s k (plus i0 i))) (\lambda (n: nat).(subst0 n
64 u0 x t0)) H5 (s k (S (plus i0 i))) (s_S k (plus i0 i))) in (ex_intro2 T
65 (\lambda (t: T).(subst0 i u1 (THead k u t3) t)) (\lambda (t: T).(subst0 (S
66 (plus i0 i)) u0 t (THead k u t0))) (THead k u x) (subst0_snd k u1 x t3 i H3
67 u) (subst0_snd k u0 t0 x (S (plus i0 i)) H6 u))))))) (H1 u1 u0 i0
68 H2)))))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u0: T).(\lambda
69 (i: nat).(\lambda (_: (subst0 i v u1 u0)).(\lambda (H1: ((\forall (u3:
70 T).(\forall (u: T).(\forall (i0: nat).((subst0 i0 u u3 v) \to (ex2 T (\lambda
71 (t: T).(subst0 i u3 u1 t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u t
72 u0))))))))).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_:
73 (subst0 (s k i) v t0 t3)).(\lambda (H3: ((\forall (u3: T).(\forall (u:
74 T).(\forall (i0: nat).((subst0 i0 u u3 v) \to (ex2 T (\lambda (t: T).(subst0
75 (s k i) u3 t0 t)) (\lambda (t: T).(subst0 (S (plus i0 (s k i))) u t
76 t3))))))))).(\lambda (u3: T).(\lambda (u: T).(\lambda (i0: nat).(\lambda (H4:
77 (subst0 i0 u u3 v)).(ex2_ind T (\lambda (t: T).(subst0 (s k i) u3 t0 t))
78 (\lambda (t: T).(subst0 (S (plus i0 (s k i))) u t t3)) (ex2 T (\lambda (t:
79 T).(subst0 i u3 (THead k u1 t0) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u
80 t (THead k u0 t3)))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i) u3 t0
81 x)).(\lambda (H6: (subst0 (S (plus i0 (s k i))) u x t3)).(ex2_ind T (\lambda
82 (t: T).(subst0 i u3 u1 t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u t u0))
83 (ex2 T (\lambda (t: T).(subst0 i u3 (THead k u1 t0) t)) (\lambda (t:
84 T).(subst0 (S (plus i0 i)) u t (THead k u0 t3)))) (\lambda (x0: T).(\lambda
85 (H7: (subst0 i u3 u1 x0)).(\lambda (H8: (subst0 (S (plus i0 i)) u x0
86 u0)).(let H9 \def (eq_ind_r nat (plus i0 (s k i)) (\lambda (n: nat).(subst0
87 (S n) u x t3)) H6 (s k (plus i0 i)) (s_plus_sym k i0 i)) in (let H10 \def
88 (eq_ind_r nat (S (s k (plus i0 i))) (\lambda (n: nat).(subst0 n u x t3)) H9
89 (s k (S (plus i0 i))) (s_S k (plus i0 i))) in (ex_intro2 T (\lambda (t:
90 T).(subst0 i u3 (THead k u1 t0) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u
91 t (THead k u0 t3))) (THead k x0 x) (subst0_both u3 u1 x0 i H7 k t0 x H5)
92 (subst0_both u x0 u0 (S (plus i0 i)) H8 k x t3 H10))))))) (H1 u3 u i0 H4)))))
93 (H3 u3 u i0 H4))))))))))))))))) j u2 t1 t2 H))))).
98 theorem subst0_subst0_back:
99 \forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0
100 j u2 t1 t2) \to (\forall (u1: T).(\forall (u: T).(\forall (i: nat).((subst0 i
101 u u2 u1) \to (ex2 T (\lambda (t: T).(subst0 j u1 t1 t)) (\lambda (t:
102 T).(subst0 (S (plus i j)) u t2 t)))))))))))
104 \lambda (t1: T).(\lambda (t2: T).(\lambda (u2: T).(\lambda (j: nat).(\lambda
105 (H: (subst0 j u2 t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t:
106 T).(\lambda (t0: T).(\lambda (t3: T).(\forall (u1: T).(\forall (u:
107 T).(\forall (i: nat).((subst0 i u t u1) \to (ex2 T (\lambda (t4: T).(subst0 n
108 u1 t0 t4)) (\lambda (t4: T).(subst0 (S (plus i n)) u t3 t4)))))))))))
109 (\lambda (v: T).(\lambda (i: nat).(\lambda (u1: T).(\lambda (u: T).(\lambda
110 (i0: nat).(\lambda (H0: (subst0 i0 u v u1)).(eq_ind nat (plus i0 (S i))
111 (\lambda (n: nat).(ex2 T (\lambda (t: T).(subst0 i u1 (TLRef i) t)) (\lambda
112 (t: T).(subst0 n u (lift (S i) O v) t)))) (ex_intro2 T (\lambda (t:
113 T).(subst0 i u1 (TLRef i) t)) (\lambda (t: T).(subst0 (plus i0 (S i)) u (lift
114 (S i) O v) t)) (lift (S i) O u1) (subst0_lref u1 i) (subst0_lift_ge v u1 u i0
115 (S i) H0 O (le_O_n i0))) (S (plus i0 i)) (sym_eq nat (S (plus i0 i)) (plus i0
116 (S i)) (plus_n_Sm i0 i))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda
117 (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u0)).(\lambda (H1:
118 ((\forall (u3: T).(\forall (u: T).(\forall (i0: nat).((subst0 i0 u v u3) \to
119 (ex2 T (\lambda (t: T).(subst0 i u3 u1 t)) (\lambda (t: T).(subst0 (S (plus
120 i0 i)) u u0 t))))))))).(\lambda (t: T).(\lambda (k: K).(\lambda (u3:
121 T).(\lambda (u: T).(\lambda (i0: nat).(\lambda (H2: (subst0 i0 u v
122 u3)).(ex2_ind T (\lambda (t0: T).(subst0 i u3 u1 t0)) (\lambda (t0:
123 T).(subst0 (S (plus i0 i)) u u0 t0)) (ex2 T (\lambda (t0: T).(subst0 i u3
124 (THead k u1 t) t0)) (\lambda (t0: T).(subst0 (S (plus i0 i)) u (THead k u0 t)
125 t0))) (\lambda (x: T).(\lambda (H3: (subst0 i u3 u1 x)).(\lambda (H4: (subst0
126 (S (plus i0 i)) u u0 x)).(ex_intro2 T (\lambda (t0: T).(subst0 i u3 (THead k
127 u1 t) t0)) (\lambda (t0: T).(subst0 (S (plus i0 i)) u (THead k u0 t) t0))
128 (THead k x t) (subst0_fst u3 x u1 i H3 t k) (subst0_fst u x u0 (S (plus i0
129 i)) H4 t k))))) (H1 u3 u i0 H2)))))))))))))) (\lambda (k: K).(\lambda (v:
130 T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (_: (subst0
131 (s k i) v t3 t0)).(\lambda (H1: ((\forall (u1: T).(\forall (u: T).(\forall
132 (i0: nat).((subst0 i0 u v u1) \to (ex2 T (\lambda (t: T).(subst0 (s k i) u1
133 t3 t)) (\lambda (t: T).(subst0 (S (plus i0 (s k i))) u t0 t))))))))).(\lambda
134 (u: T).(\lambda (u1: T).(\lambda (u0: T).(\lambda (i0: nat).(\lambda (H2:
135 (subst0 i0 u0 v u1)).(ex2_ind T (\lambda (t: T).(subst0 (s k i) u1 t3 t))
136 (\lambda (t: T).(subst0 (S (plus i0 (s k i))) u0 t0 t)) (ex2 T (\lambda (t:
137 T).(subst0 i u1 (THead k u t3) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u0
138 (THead k u t0) t))) (\lambda (x: T).(\lambda (H3: (subst0 (s k i) u1 t3
139 x)).(\lambda (H4: (subst0 (S (plus i0 (s k i))) u0 t0 x)).(let H5 \def
140 (eq_ind_r nat (plus i0 (s k i)) (\lambda (n: nat).(subst0 (S n) u0 t0 x)) H4
141 (s k (plus i0 i)) (s_plus_sym k i0 i)) in (let H6 \def (eq_ind_r nat (S (s k
142 (plus i0 i))) (\lambda (n: nat).(subst0 n u0 t0 x)) H5 (s k (S (plus i0 i)))
143 (s_S k (plus i0 i))) in (ex_intro2 T (\lambda (t: T).(subst0 i u1 (THead k u
144 t3) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u0 (THead k u t0) t)) (THead
145 k u x) (subst0_snd k u1 x t3 i H3 u) (subst0_snd k u0 x t0 (S (plus i0 i)) H6
146 u))))))) (H1 u1 u0 i0 H2)))))))))))))) (\lambda (v: T).(\lambda (u1:
147 T).(\lambda (u0: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1
148 u0)).(\lambda (H1: ((\forall (u3: T).(\forall (u: T).(\forall (i0:
149 nat).((subst0 i0 u v u3) \to (ex2 T (\lambda (t: T).(subst0 i u3 u1 t))
150 (\lambda (t: T).(subst0 (S (plus i0 i)) u u0 t))))))))).(\lambda (k:
151 K).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (subst0 (s k i) v t0
152 t3)).(\lambda (H3: ((\forall (u3: T).(\forall (u: T).(\forall (i0:
153 nat).((subst0 i0 u v u3) \to (ex2 T (\lambda (t: T).(subst0 (s k i) u3 t0 t))
154 (\lambda (t: T).(subst0 (S (plus i0 (s k i))) u t3 t))))))))).(\lambda (u3:
155 T).(\lambda (u: T).(\lambda (i0: nat).(\lambda (H4: (subst0 i0 u v
156 u3)).(ex2_ind T (\lambda (t: T).(subst0 (s k i) u3 t0 t)) (\lambda (t:
157 T).(subst0 (S (plus i0 (s k i))) u t3 t)) (ex2 T (\lambda (t: T).(subst0 i u3
158 (THead k u1 t0) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u (THead k u0 t3)
159 t))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i) u3 t0 x)).(\lambda (H6:
160 (subst0 (S (plus i0 (s k i))) u t3 x)).(ex2_ind T (\lambda (t: T).(subst0 i
161 u3 u1 t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u u0 t)) (ex2 T (\lambda
162 (t: T).(subst0 i u3 (THead k u1 t0) t)) (\lambda (t: T).(subst0 (S (plus i0
163 i)) u (THead k u0 t3) t))) (\lambda (x0: T).(\lambda (H7: (subst0 i u3 u1
164 x0)).(\lambda (H8: (subst0 (S (plus i0 i)) u u0 x0)).(let H9 \def (eq_ind_r
165 nat (plus i0 (s k i)) (\lambda (n: nat).(subst0 (S n) u t3 x)) H6 (s k (plus
166 i0 i)) (s_plus_sym k i0 i)) in (let H10 \def (eq_ind_r nat (S (s k (plus i0
167 i))) (\lambda (n: nat).(subst0 n u t3 x)) H9 (s k (S (plus i0 i))) (s_S k
168 (plus i0 i))) in (ex_intro2 T (\lambda (t: T).(subst0 i u3 (THead k u1 t0)
169 t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u (THead k u0 t3) t)) (THead k x0
170 x) (subst0_both u3 u1 x0 i H7 k t0 x H5) (subst0_both u u0 x0 (S (plus i0 i))
171 H8 k t3 x H10))))))) (H1 u3 u i0 H4))))) (H3 u3 u i0 H4))))))))))))))))) j u2
177 theorem subst0_trans:
178 \forall (t2: T).(\forall (t1: T).(\forall (v: T).(\forall (i: nat).((subst0
179 i v t1 t2) \to (\forall (t3: T).((subst0 i v t2 t3) \to (subst0 i v t1
182 \lambda (t2: T).(\lambda (t1: T).(\lambda (v: T).(\lambda (i: nat).(\lambda
183 (H: (subst0 i v t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t:
184 T).(\lambda (t0: T).(\lambda (t3: T).(\forall (t4: T).((subst0 n t t3 t4) \to
185 (subst0 n t t0 t4))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (t3:
186 T).(\lambda (H0: (subst0 i0 v0 (lift (S i0) O v0) t3)).(subst0_gen_lift_false
187 v0 v0 t3 (S i0) O i0 (le_O_n i0) (le_n (plus O (S i0))) H0 (subst0 i0 v0
188 (TLRef i0) t3)))))) (\lambda (v0: T).(\lambda (u2: T).(\lambda (u1:
189 T).(\lambda (i0: nat).(\lambda (H0: (subst0 i0 v0 u1 u2)).(\lambda (H1:
190 ((\forall (t3: T).((subst0 i0 v0 u2 t3) \to (subst0 i0 v0 u1 t3))))).(\lambda
191 (t: T).(\lambda (k: K).(\lambda (t3: T).(\lambda (H2: (subst0 i0 v0 (THead k
192 u2 t) t3)).(or3_ind (ex2 T (\lambda (u3: T).(eq T t3 (THead k u3 t)))
193 (\lambda (u3: T).(subst0 i0 v0 u2 u3))) (ex2 T (\lambda (t4: T).(eq T t3
194 (THead k u2 t4))) (\lambda (t4: T).(subst0 (s k i0) v0 t t4))) (ex3_2 T T
195 (\lambda (u3: T).(\lambda (t4: T).(eq T t3 (THead k u3 t4)))) (\lambda (u3:
196 T).(\lambda (_: T).(subst0 i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t4:
197 T).(subst0 (s k i0) v0 t t4)))) (subst0 i0 v0 (THead k u1 t) t3) (\lambda
198 (H3: (ex2 T (\lambda (u3: T).(eq T t3 (THead k u3 t))) (\lambda (u3:
199 T).(subst0 i0 v0 u2 u3)))).(ex2_ind T (\lambda (u3: T).(eq T t3 (THead k u3
200 t))) (\lambda (u3: T).(subst0 i0 v0 u2 u3)) (subst0 i0 v0 (THead k u1 t) t3)
201 (\lambda (x: T).(\lambda (H4: (eq T t3 (THead k x t))).(\lambda (H5: (subst0
202 i0 v0 u2 x)).(eq_ind_r T (THead k x t) (\lambda (t0: T).(subst0 i0 v0 (THead
203 k u1 t) t0)) (subst0_fst v0 x u1 i0 (H1 x H5) t k) t3 H4)))) H3)) (\lambda
204 (H3: (ex2 T (\lambda (t4: T).(eq T t3 (THead k u2 t4))) (\lambda (t4:
205 T).(subst0 (s k i0) v0 t t4)))).(ex2_ind T (\lambda (t4: T).(eq T t3 (THead k
206 u2 t4))) (\lambda (t4: T).(subst0 (s k i0) v0 t t4)) (subst0 i0 v0 (THead k
207 u1 t) t3) (\lambda (x: T).(\lambda (H4: (eq T t3 (THead k u2 x))).(\lambda
208 (H5: (subst0 (s k i0) v0 t x)).(eq_ind_r T (THead k u2 x) (\lambda (t0:
209 T).(subst0 i0 v0 (THead k u1 t) t0)) (subst0_both v0 u1 u2 i0 H0 k t x H5) t3
210 H4)))) H3)) (\lambda (H3: (ex3_2 T T (\lambda (u3: T).(\lambda (t4: T).(eq T
211 t3 (THead k u3 t4)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v0 u2 u3)))
212 (\lambda (_: T).(\lambda (t4: T).(subst0 (s k i0) v0 t t4))))).(ex3_2_ind T T
213 (\lambda (u3: T).(\lambda (t4: T).(eq T t3 (THead k u3 t4)))) (\lambda (u3:
214 T).(\lambda (_: T).(subst0 i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t4:
215 T).(subst0 (s k i0) v0 t t4))) (subst0 i0 v0 (THead k u1 t) t3) (\lambda (x0:
216 T).(\lambda (x1: T).(\lambda (H4: (eq T t3 (THead k x0 x1))).(\lambda (H5:
217 (subst0 i0 v0 u2 x0)).(\lambda (H6: (subst0 (s k i0) v0 t x1)).(eq_ind_r T
218 (THead k x0 x1) (\lambda (t0: T).(subst0 i0 v0 (THead k u1 t) t0))
219 (subst0_both v0 u1 x0 i0 (H1 x0 H5) k t x1 H6) t3 H4)))))) H3))
220 (subst0_gen_head k v0 u2 t t3 i0 H2)))))))))))) (\lambda (k: K).(\lambda (v0:
221 T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (H0: (subst0
222 (s k i0) v0 t3 t0)).(\lambda (H1: ((\forall (t4: T).((subst0 (s k i0) v0 t0
223 t4) \to (subst0 (s k i0) v0 t3 t4))))).(\lambda (u: T).(\lambda (t4:
224 T).(\lambda (H2: (subst0 i0 v0 (THead k u t0) t4)).(or3_ind (ex2 T (\lambda
225 (u2: T).(eq T t4 (THead k u2 t0))) (\lambda (u2: T).(subst0 i0 v0 u u2)))
226 (ex2 T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s
227 k i0) v0 t0 t5))) (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
228 (THead k u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v0 u u2)))
229 (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i0) v0 t0 t5)))) (subst0 i0 v0
230 (THead k u t3) t4) (\lambda (H3: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2
231 t0))) (\lambda (u2: T).(subst0 i0 v0 u u2)))).(ex2_ind T (\lambda (u2: T).(eq
232 T t4 (THead k u2 t0))) (\lambda (u2: T).(subst0 i0 v0 u u2)) (subst0 i0 v0
233 (THead k u t3) t4) (\lambda (x: T).(\lambda (H4: (eq T t4 (THead k x
234 t0))).(\lambda (H5: (subst0 i0 v0 u x)).(eq_ind_r T (THead k x t0) (\lambda
235 (t: T).(subst0 i0 v0 (THead k u t3) t)) (subst0_both v0 u x i0 H5 k t3 t0 H0)
236 t4 H4)))) H3)) (\lambda (H3: (ex2 T (\lambda (t5: T).(eq T t4 (THead k u
237 t5))) (\lambda (t5: T).(subst0 (s k i0) v0 t0 t5)))).(ex2_ind T (\lambda (t5:
238 T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i0) v0 t0 t5))
239 (subst0 i0 v0 (THead k u t3) t4) (\lambda (x: T).(\lambda (H4: (eq T t4
240 (THead k u x))).(\lambda (H5: (subst0 (s k i0) v0 t0 x)).(eq_ind_r T (THead k
241 u x) (\lambda (t: T).(subst0 i0 v0 (THead k u t3) t)) (subst0_snd k v0 x t3
242 i0 (H1 x H5) u) t4 H4)))) H3)) (\lambda (H3: (ex3_2 T T (\lambda (u2:
243 T).(\lambda (t5: T).(eq T t4 (THead k u2 t5)))) (\lambda (u2: T).(\lambda (_:
244 T).(subst0 i0 v0 u u2))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i0) v0
245 t0 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead k
246 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v0 u u2))) (\lambda (_:
247 T).(\lambda (t5: T).(subst0 (s k i0) v0 t0 t5))) (subst0 i0 v0 (THead k u t3)
248 t4) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t4 (THead k x0
249 x1))).(\lambda (H5: (subst0 i0 v0 u x0)).(\lambda (H6: (subst0 (s k i0) v0 t0
250 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(subst0 i0 v0 (THead k u t3)
251 t)) (subst0_both v0 u x0 i0 H5 k t3 x1 (H1 x1 H6)) t4 H4)))))) H3))
252 (subst0_gen_head k v0 u t0 t4 i0 H2)))))))))))) (\lambda (v0: T).(\lambda
253 (u1: T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda (H0: (subst0 i0 v0 u1
254 u2)).(\lambda (H1: ((\forall (t3: T).((subst0 i0 v0 u2 t3) \to (subst0 i0 v0
255 u1 t3))))).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H2:
256 (subst0 (s k i0) v0 t0 t3)).(\lambda (H3: ((\forall (t4: T).((subst0 (s k i0)
257 v0 t3 t4) \to (subst0 (s k i0) v0 t0 t4))))).(\lambda (t4: T).(\lambda (H4:
258 (subst0 i0 v0 (THead k u2 t3) t4)).(or3_ind (ex2 T (\lambda (u3: T).(eq T t4
259 (THead k u3 t3))) (\lambda (u3: T).(subst0 i0 v0 u2 u3))) (ex2 T (\lambda
260 (t5: T).(eq T t4 (THead k u2 t5))) (\lambda (t5: T).(subst0 (s k i0) v0 t3
261 t5))) (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3
262 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v0 u2 u3))) (\lambda (_:
263 T).(\lambda (t5: T).(subst0 (s k i0) v0 t3 t5)))) (subst0 i0 v0 (THead k u1
264 t0) t4) (\lambda (H5: (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3 t3)))
265 (\lambda (u3: T).(subst0 i0 v0 u2 u3)))).(ex2_ind T (\lambda (u3: T).(eq T t4
266 (THead k u3 t3))) (\lambda (u3: T).(subst0 i0 v0 u2 u3)) (subst0 i0 v0 (THead
267 k u1 t0) t4) (\lambda (x: T).(\lambda (H6: (eq T t4 (THead k x t3))).(\lambda
268 (H7: (subst0 i0 v0 u2 x)).(eq_ind_r T (THead k x t3) (\lambda (t: T).(subst0
269 i0 v0 (THead k u1 t0) t)) (subst0_both v0 u1 x i0 (H1 x H7) k t0 t3 H2) t4
270 H6)))) H5)) (\lambda (H5: (ex2 T (\lambda (t5: T).(eq T t4 (THead k u2 t5)))
271 (\lambda (t5: T).(subst0 (s k i0) v0 t3 t5)))).(ex2_ind T (\lambda (t5:
272 T).(eq T t4 (THead k u2 t5))) (\lambda (t5: T).(subst0 (s k i0) v0 t3 t5))
273 (subst0 i0 v0 (THead k u1 t0) t4) (\lambda (x: T).(\lambda (H6: (eq T t4
274 (THead k u2 x))).(\lambda (H7: (subst0 (s k i0) v0 t3 x)).(eq_ind_r T (THead
275 k u2 x) (\lambda (t: T).(subst0 i0 v0 (THead k u1 t0) t)) (subst0_both v0 u1
276 u2 i0 H0 k t0 x (H3 x H7)) t4 H6)))) H5)) (\lambda (H5: (ex3_2 T T (\lambda
277 (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3:
278 T).(\lambda (_: T).(subst0 i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t5:
279 T).(subst0 (s k i0) v0 t3 t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda
280 (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0
281 i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i0) v0 t3 t5)))
282 (subst0 i0 v0 (THead k u1 t0) t4) (\lambda (x0: T).(\lambda (x1: T).(\lambda
283 (H6: (eq T t4 (THead k x0 x1))).(\lambda (H7: (subst0 i0 v0 u2 x0)).(\lambda
284 (H8: (subst0 (s k i0) v0 t3 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t:
285 T).(subst0 i0 v0 (THead k u1 t0) t)) (subst0_both v0 u1 x0 i0 (H1 x0 H7) k t0
286 x1 (H3 x1 H8)) t4 H6)))))) H5)) (subst0_gen_head k v0 u2 t3 t4 i0
287 H4))))))))))))))) i v t1 t2 H))))).
292 theorem subst0_confluence_neq:
293 \forall (t0: T).(\forall (t1: T).(\forall (u1: T).(\forall (i1:
294 nat).((subst0 i1 u1 t0 t1) \to (\forall (t2: T).(\forall (u2: T).(\forall
295 (i2: nat).((subst0 i2 u2 t0 t2) \to ((not (eq nat i1 i2)) \to (ex2 T (\lambda
296 (t: T).(subst0 i2 u2 t1 t)) (\lambda (t: T).(subst0 i1 u1 t2 t))))))))))))
298 \lambda (t0: T).(\lambda (t1: T).(\lambda (u1: T).(\lambda (i1:
299 nat).(\lambda (H: (subst0 i1 u1 t0 t1)).(subst0_ind (\lambda (n:
300 nat).(\lambda (t: T).(\lambda (t2: T).(\lambda (t3: T).(\forall (t4:
301 T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq
302 nat n i2)) \to (ex2 T (\lambda (t5: T).(subst0 i2 u2 t3 t5)) (\lambda (t5:
303 T).(subst0 n t t4 t5)))))))))))) (\lambda (v: T).(\lambda (i: nat).(\lambda
304 (t2: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H0: (subst0 i2 u2
305 (TLRef i) t2)).(\lambda (H1: (not (eq nat i i2))).(land_ind (eq nat i i2) (eq
306 T t2 (lift (S i) O u2)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v)
307 t)) (\lambda (t: T).(subst0 i v t2 t))) (\lambda (H2: (eq nat i i2)).(\lambda
308 (H3: (eq T t2 (lift (S i) O u2))).(let H4 \def (eq_ind nat i (\lambda (n:
309 nat).(not (eq nat n i2))) H1 i2 H2) in (eq_ind_r T (lift (S i) O u2) (\lambda
310 (t: T).(ex2 T (\lambda (t3: T).(subst0 i2 u2 (lift (S i) O v) t3)) (\lambda
311 (t3: T).(subst0 i v t t3)))) (let H5 \def (match (H4 (refl_equal nat i2)) in
312 False return (\lambda (_: False).(ex2 T (\lambda (t: T).(subst0 i2 u2 (lift
313 (S i) O v) t)) (\lambda (t: T).(subst0 i v (lift (S i) O u2) t)))) with [])
314 in H5) t2 H3)))) (subst0_gen_lref u2 t2 i2 i H0))))))))) (\lambda (v:
315 T).(\lambda (u2: T).(\lambda (u0: T).(\lambda (i: nat).(\lambda (H0: (subst0
316 i v u0 u2)).(\lambda (H1: ((\forall (t2: T).(\forall (u3: T).(\forall (i2:
317 nat).((subst0 i2 u3 u0 t2) \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t:
318 T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda
319 (t: T).(\lambda (k: K).(\lambda (t2: T).(\lambda (u3: T).(\lambda (i2:
320 nat).(\lambda (H2: (subst0 i2 u3 (THead k u0 t) t2)).(\lambda (H3: (not (eq
321 nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq T t2 (THead k u4 t)))
322 (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T (\lambda (t3: T).(eq T t2
323 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex3_2 T T
324 (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4:
325 T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3:
326 T).(subst0 (s k i2) u3 t t3)))) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead
327 k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (H4: (ex2 T
328 (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4: T).(subst0 i2 u3 u0
329 u4)))).(ex2_ind T (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4:
330 T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t)
331 t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq
332 T t2 (THead k x t))).(\lambda (H6: (subst0 i2 u3 u0 x)).(eq_ind_r T (THead k
333 x t) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t)
334 t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex2_ind T (\lambda (t3:
335 T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i v x t3)) (ex2 T (\lambda
336 (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead
337 k x t) t3))) (\lambda (x0: T).(\lambda (H7: (subst0 i2 u3 u2 x0)).(\lambda
338 (H8: (subst0 i v x x0)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k
339 u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x t) t3)) (THead k x0 t)
340 (subst0_fst u3 x0 u2 i2 H7 t k) (subst0_fst v x0 x i H8 t k))))) (H1 x u3 i2
341 H6 H3)) t2 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t3: T).(eq T t2 (THead
342 k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3)))).(ex2_ind T (\lambda
343 (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t
344 t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3:
345 T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq T t2 (THead k u0
346 x))).(\lambda (H6: (subst0 (s k i2) u3 t x)).(eq_ind_r T (THead k u0 x)
347 (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4))
348 (\lambda (t4: T).(subst0 i v t3 t4)))) (ex_intro2 T (\lambda (t3: T).(subst0
349 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k u0 x) t3))
350 (THead k u2 x) (subst0_snd k u3 x t i2 H6 u2) (subst0_fst v u2 u0 i H0 x k))
351 t2 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u4: T).(\lambda (t3: T).(eq
352 T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0
353 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t
354 t3))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4
355 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_:
356 T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex2 T (\lambda (t3:
357 T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3)))
358 (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t2 (THead k x0
359 x1))).(\lambda (H6: (subst0 i2 u3 u0 x0)).(\lambda (H7: (subst0 (s k i2) u3 t
360 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(ex2 T (\lambda (t4:
361 T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4))))
362 (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i
363 v x0 t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda
364 (t3: T).(subst0 i v (THead k x0 x1) t3))) (\lambda (x: T).(\lambda (H8:
365 (subst0 i2 u3 u2 x)).(\lambda (H9: (subst0 i v x0 x)).(ex_intro2 T (\lambda
366 (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead
367 k x0 x1) t3)) (THead k x x1) (subst0_both u3 u2 x i2 H8 k t x1 H7)
368 (subst0_fst v x x0 i H9 x1 k))))) (H1 x0 u3 i2 H6 H3)) t2 H5)))))) H4))
369 (subst0_gen_head k u3 u0 t t2 i2 H2))))))))))))))) (\lambda (k: K).(\lambda
370 (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H0:
371 (subst0 (s k i) v t3 t2)).(\lambda (H1: ((\forall (t4: T).(\forall (u2:
372 T).(\forall (i2: nat).((subst0 i2 u2 t3 t4) \to ((not (eq nat (s k i) i2))
373 \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t2 t)) (\lambda (t: T).(subst0 (s k
374 i) v t4 t)))))))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (u2:
375 T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u2 (THead k u t3)
376 t4)).(\lambda (H3: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u3: T).(eq
377 T t4 (THead k u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3))) (ex2 T (\lambda
378 (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2) u2 t3
379 t5))) (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3
380 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_:
381 T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5)))) (ex2 T (\lambda (t:
382 T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t)))
383 (\lambda (H4: (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3 t3))) (\lambda
384 (u3: T).(subst0 i2 u2 u u3)))).(ex2_ind T (\lambda (u3: T).(eq T t4 (THead k
385 u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3)) (ex2 T (\lambda (t: T).(subst0
386 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x:
387 T).(\lambda (H5: (eq T t4 (THead k x t3))).(\lambda (H6: (subst0 i2 u2 u
388 x)).(eq_ind_r T (THead k x t3) (\lambda (t: T).(ex2 T (\lambda (t5:
389 T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5))))
390 (ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t:
391 T).(subst0 i v (THead k x t3) t)) (THead k x t2) (subst0_fst u2 x u i2 H6 t2
392 k) (subst0_snd k v t2 t3 i H0 x)) t4 H5)))) H4)) (\lambda (H4: (ex2 T
393 (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2)
394 u2 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda
395 (t5: T).(subst0 (s k i2) u2 t3 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u2
396 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x:
397 T).(\lambda (H5: (eq T t4 (THead k u x))).(\lambda (H6: (subst0 (s k i2) u2
398 t3 x)).(eq_ind_r T (THead k u x) (\lambda (t: T).(ex2 T (\lambda (t5:
399 T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5))))
400 (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0
401 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t))
402 (\lambda (t: T).(subst0 i v (THead k u x) t))) (\lambda (x0: T).(\lambda (H7:
403 (subst0 (s k i2) u2 t2 x0)).(\lambda (H8: (subst0 (s k i) v x x0)).(ex_intro2
404 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i
405 v (THead k u x) t)) (THead k u x0) (subst0_snd k u2 x0 t2 i2 H7 u)
406 (subst0_snd k v x0 x i H8 u))))) (H1 x u2 (s k i2) H6 (ex2_ind T (\lambda (t:
407 T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x t)) ((eq
408 nat (s k i) (s k i2)) \to False) (\lambda (x0: T).(\lambda (_: (subst0 (s k
409 i2) u2 t2 x0)).(\lambda (_: (subst0 (s k i) v x x0)).(\lambda (H9: (eq nat (s
410 k i) (s k i2))).(H3 (s_inj k i i2 H9)))))) (H1 x u2 (s k i2) H6 (\lambda (H7:
411 (eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H7))))))) t4 H5)))) H4))
412 (\lambda (H4: (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k
413 u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_:
414 T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))))).(ex3_2_ind T T (\lambda
415 (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3:
416 T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5:
417 T).(subst0 (s k i2) u2 t3 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k
418 u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1:
419 T).(\lambda (H5: (eq T t4 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u2 u
420 x0)).(\lambda (H7: (subst0 (s k i2) u2 t3 x1)).(eq_ind_r T (THead k x0 x1)
421 (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5))
422 (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k
423 i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t:
424 T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0
425 x1) t))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i2) u2 t2 x)).(\lambda
426 (H9: (subst0 (s k i) v x1 x)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2
427 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k
428 x0 x) (subst0_both u2 u x0 i2 H6 k t2 x H8) (subst0_snd k v x x1 i H9 x0)))))
429 (H1 x1 u2 (s k i2) H7 (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t))
430 (\lambda (t: T).(subst0 (s k i) v x1 t)) ((eq nat (s k i) (s k i2)) \to
431 False) (\lambda (x: T).(\lambda (_: (subst0 (s k i2) u2 t2 x)).(\lambda (_:
432 (subst0 (s k i) v x1 x)).(\lambda (H10: (eq nat (s k i) (s k i2))).(H3 (s_inj
433 k i i2 H10)))))) (H1 x1 u2 (s k i2) H7 (\lambda (H8: (eq nat (s k i) (s k
434 i2))).(H3 (s_inj k i i2 H8))))))) t4 H5)))))) H4)) (subst0_gen_head k u2 u t3
435 t4 i2 H2))))))))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda (u2:
436 T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1:
437 ((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2)
438 \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t))
439 (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (k: K).(\lambda (t2:
440 T).(\lambda (t3: T).(\lambda (H2: (subst0 (s k i) v t2 t3)).(\lambda (H3:
441 ((\forall (t4: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 t2 t4)
442 \to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 t3
443 t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (t4:
444 T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H4: (subst0 i2 u3 (THead k
445 u0 t2) t4)).(\lambda (H5: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4:
446 T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T
447 (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2)
448 u3 t2 t5))) (ex3_2 T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4
449 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_:
450 T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5)))) (ex2 T (\lambda (t:
451 T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t)))
452 (\lambda (H6: (ex2 T (\lambda (u4: T).(eq T t4 (THead k u4 t2))) (\lambda
453 (u4: T).(subst0 i2 u3 u0 u4)))).(ex2_ind T (\lambda (u4: T).(eq T t4 (THead k
454 u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t:
455 T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t)))
456 (\lambda (x: T).(\lambda (H7: (eq T t4 (THead k x t2))).(\lambda (H8: (subst0
457 i2 u3 u0 x)).(eq_ind_r T (THead k x t2) (\lambda (t: T).(ex2 T (\lambda (t5:
458 T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5))))
459 (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v x
460 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t:
461 T).(subst0 i v (THead k x t2) t))) (\lambda (x0: T).(\lambda (H9: (subst0 i2
462 u3 u2 x0)).(\lambda (H10: (subst0 i v x x0)).(ex_intro2 T (\lambda (t:
463 T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x
464 t2) t)) (THead k x0 t3) (subst0_fst u3 x0 u2 i2 H9 t3 k) (subst0_both v x x0
465 i H10 k t2 t3 H2))))) (H1 x u3 i2 H8 H5)) t4 H7)))) H6)) (\lambda (H6: (ex2 T
466 (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2)
467 u3 t2 t5)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda
468 (t5: T).(subst0 (s k i2) u3 t2 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u3
469 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x:
470 T).(\lambda (H7: (eq T t4 (THead k u0 x))).(\lambda (H8: (subst0 (s k i2) u3
471 t2 x)).(eq_ind_r T (THead k u0 x) (\lambda (t: T).(ex2 T (\lambda (t5:
472 T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5))))
473 (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0
474 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t))
475 (\lambda (t: T).(subst0 i v (THead k u0 x) t))) (\lambda (x0: T).(\lambda
476 (H9: (subst0 (s k i2) u3 t3 x0)).(\lambda (H10: (subst0 (s k i) v x
477 x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda
478 (t: T).(subst0 i v (THead k u0 x) t)) (THead k u2 x0) (subst0_snd k u3 x0 t3
479 i2 H9 u2) (subst0_both v u0 u2 i H0 k x x0 H10))))) (H3 x u3 (s k i2) H8
480 (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0
481 (s k i) v x t)) ((eq nat (s k i) (s k i2)) \to False) (\lambda (x0:
482 T).(\lambda (_: (subst0 (s k i2) u3 t3 x0)).(\lambda (_: (subst0 (s k i) v x
483 x0)).(\lambda (H11: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H11))))))
484 (H3 x u3 (s k i2) H8 (\lambda (H9: (eq nat (s k i) (s k i2))).(H5 (s_inj k i
485 i2 H9))))))) t4 H7)))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u4:
486 T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_:
487 T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2)
488 u3 t2 t5))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4
489 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4)))
490 (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex2 T (\lambda
491 (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t)))
492 (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T t4 (THead k x0
493 x1))).(\lambda (H8: (subst0 i2 u3 u0 x0)).(\lambda (H9: (subst0 (s k i2) u3
494 t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5:
495 T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5))))
496 (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v
497 x0 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t:
498 T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H10: (subst0 i2
499 u3 u2 x)).(\lambda (H11: (subst0 i v x0 x)).(ex2_ind T (\lambda (t:
500 T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T
501 (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v
502 (THead k x0 x1) t))) (\lambda (x2: T).(\lambda (H12: (subst0 (s k i2) u3 t3
503 x2)).(\lambda (H13: (subst0 (s k i) v x1 x2)).(ex_intro2 T (\lambda (t:
504 T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0
505 x1) t)) (THead k x x2) (subst0_both u3 u2 x i2 H10 k t3 x2 H12) (subst0_both
506 v x0 x i H11 k x1 x2 H13))))) (H3 x1 u3 (s k i2) H9 (ex2_ind T (\lambda (t:
507 T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) ((eq
508 nat (s k i) (s k i2)) \to False) (\lambda (x2: T).(\lambda (_: (subst0 (s k
509 i2) u3 t3 x2)).(\lambda (_: (subst0 (s k i) v x1 x2)).(\lambda (H14: (eq nat
510 (s k i) (s k i2))).(H5 (s_inj k i i2 H14)))))) (H3 x1 u3 (s k i2) H9 (\lambda
511 (H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))))) (H1 x0 u3 i2
512 H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2
513 H4)))))))))))))))))) i1 u1 t0 t1 H))))).
518 theorem subst0_confluence_eq:
519 \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0
520 i u t0 t1) \to (\forall (t2: T).((subst0 i u t0 t2) \to (or4 (eq T t1 t2)
521 (ex2 T (\lambda (t: T).(subst0 i u t1 t)) (\lambda (t: T).(subst0 i u t2 t)))
522 (subst0 i u t1 t2) (subst0 i u t2 t1))))))))
524 \lambda (t0: T).(\lambda (t1: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
525 (H: (subst0 i u t0 t1)).(subst0_ind (\lambda (n: nat).(\lambda (t:
526 T).(\lambda (t2: T).(\lambda (t3: T).(\forall (t4: T).((subst0 n t t2 t4) \to
527 (or4 (eq T t3 t4) (ex2 T (\lambda (t5: T).(subst0 n t t3 t5)) (\lambda (t5:
528 T).(subst0 n t t4 t5))) (subst0 n t t3 t4) (subst0 n t t4 t3)))))))) (\lambda
529 (v: T).(\lambda (i0: nat).(\lambda (t2: T).(\lambda (H0: (subst0 i0 v (TLRef
530 i0) t2)).(land_ind (eq nat i0 i0) (eq T t2 (lift (S i0) O v)) (or4 (eq T
531 (lift (S i0) O v) t2) (ex2 T (\lambda (t: T).(subst0 i0 v (lift (S i0) O v)
532 t)) (\lambda (t: T).(subst0 i0 v t2 t))) (subst0 i0 v (lift (S i0) O v) t2)
533 (subst0 i0 v t2 (lift (S i0) O v))) (\lambda (_: (eq nat i0 i0)).(\lambda
534 (H2: (eq T t2 (lift (S i0) O v))).(or4_intro0 (eq T (lift (S i0) O v) t2)
535 (ex2 T (\lambda (t: T).(subst0 i0 v (lift (S i0) O v) t)) (\lambda (t:
536 T).(subst0 i0 v t2 t))) (subst0 i0 v (lift (S i0) O v) t2) (subst0 i0 v t2
537 (lift (S i0) O v)) (sym_eq T t2 (lift (S i0) O v) H2)))) (subst0_gen_lref v
538 t2 i0 i0 H0)))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda
539 (i0: nat).(\lambda (H0: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (t2:
540 T).((subst0 i0 v u1 t2) \to (or4 (eq T u2 t2) (ex2 T (\lambda (t: T).(subst0
541 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v t2 t))) (subst0 i0 v u2 t2) (subst0
542 i0 v t2 u2)))))).(\lambda (t: T).(\lambda (k: K).(\lambda (t2: T).(\lambda
543 (H2: (subst0 i0 v (THead k u1 t) t2)).(or3_ind (ex2 T (\lambda (u3: T).(eq T
544 t2 (THead k u3 t))) (\lambda (u3: T).(subst0 i0 v u1 u3))) (ex2 T (\lambda
545 (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i0) v t
546 t3))) (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead k u3
547 t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_:
548 T).(\lambda (t3: T).(subst0 (s k i0) v t t3)))) (or4 (eq T (THead k u2 t) t2)
549 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
550 T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2
551 (THead k u2 t))) (\lambda (H3: (ex2 T (\lambda (u3: T).(eq T t2 (THead k u3
552 t))) (\lambda (u3: T).(subst0 i0 v u1 u3)))).(ex2_ind T (\lambda (u3: T).(eq
553 T t2 (THead k u3 t))) (\lambda (u3: T).(subst0 i0 v u1 u3)) (or4 (eq T (THead
554 k u2 t) t2) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda
555 (t3: T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2
556 (THead k u2 t))) (\lambda (x: T).(\lambda (H4: (eq T t2 (THead k x
557 t))).(\lambda (H5: (subst0 i0 v u1 x)).(eq_ind_r T (THead k x t) (\lambda
558 (t3: T).(or4 (eq T (THead k u2 t) t3) (ex2 T (\lambda (t4: T).(subst0 i0 v
559 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i0 v t3 t4))) (subst0 i0 v
560 (THead k u2 t) t3) (subst0 i0 v t3 (THead k u2 t)))) (or4_ind (eq T u2 x)
561 (ex2 T (\lambda (t3: T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v x
562 t3))) (subst0 i0 v u2 x) (subst0 i0 v x u2) (or4 (eq T (THead k u2 t) (THead
563 k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda
564 (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t) (THead k
565 x t)) (subst0 i0 v (THead k x t) (THead k u2 t))) (\lambda (H6: (eq T u2
566 x)).(eq_ind_r T x (\lambda (t3: T).(or4 (eq T (THead k t3 t) (THead k x t))
567 (ex2 T (\lambda (t4: T).(subst0 i0 v (THead k t3 t) t4)) (\lambda (t4:
568 T).(subst0 i0 v (THead k x t) t4))) (subst0 i0 v (THead k t3 t) (THead k x
569 t)) (subst0 i0 v (THead k x t) (THead k t3 t)))) (or4_intro0 (eq T (THead k x
570 t) (THead k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k x t) t3))
571 (\lambda (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k x t)
572 (THead k x t)) (subst0 i0 v (THead k x t) (THead k x t)) (refl_equal T (THead
573 k x t))) u2 H6)) (\lambda (H6: (ex2 T (\lambda (t3: T).(subst0 i0 v u2 t3))
574 (\lambda (t3: T).(subst0 i0 v x t3)))).(ex2_ind T (\lambda (t3: T).(subst0 i0
575 v u2 t3)) (\lambda (t3: T).(subst0 i0 v x t3)) (or4 (eq T (THead k u2 t)
576 (THead k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
577 (\lambda (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t)
578 (THead k x t)) (subst0 i0 v (THead k x t) (THead k u2 t))) (\lambda (x0:
579 T).(\lambda (H7: (subst0 i0 v u2 x0)).(\lambda (H8: (subst0 i0 v x
580 x0)).(or4_intro1 (eq T (THead k u2 t) (THead k x t)) (ex2 T (\lambda (t3:
581 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x
582 t) t3))) (subst0 i0 v (THead k u2 t) (THead k x t)) (subst0 i0 v (THead k x
583 t) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t)
584 t3)) (\lambda (t3: T).(subst0 i0 v (THead k x t) t3)) (THead k x0 t)
585 (subst0_fst v x0 u2 i0 H7 t k) (subst0_fst v x0 x i0 H8 t k)))))) H6))
586 (\lambda (H6: (subst0 i0 v u2 x)).(or4_intro2 (eq T (THead k u2 t) (THead k x
587 t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
588 T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t) (THead k x
589 t)) (subst0 i0 v (THead k x t) (THead k u2 t)) (subst0_fst v x u2 i0 H6 t
590 k))) (\lambda (H6: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t)
591 (THead k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
592 (\lambda (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t)
593 (THead k x t)) (subst0 i0 v (THead k x t) (THead k u2 t)) (subst0_fst v u2 x
594 i0 H6 t k))) (H1 x H5)) t2 H4)))) H3)) (\lambda (H3: (ex2 T (\lambda (t3:
595 T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i0) v t
596 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
597 T).(subst0 (s k i0) v t t3)) (or4 (eq T (THead k u2 t) t2) (ex2 T (\lambda
598 (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v t2
599 t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2 (THead k u2 t)))
600 (\lambda (x: T).(\lambda (H4: (eq T t2 (THead k u1 x))).(\lambda (H5: (subst0
601 (s k i0) v t x)).(eq_ind_r T (THead k u1 x) (\lambda (t3: T).(or4 (eq T
602 (THead k u2 t) t3) (ex2 T (\lambda (t4: T).(subst0 i0 v (THead k u2 t) t4))
603 (\lambda (t4: T).(subst0 i0 v t3 t4))) (subst0 i0 v (THead k u2 t) t3)
604 (subst0 i0 v t3 (THead k u2 t)))) (or4_ind (eq T u2 u2) (ex2 T (\lambda (t3:
605 T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3))) (subst0 i0 v
606 u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T
607 (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0
608 v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0
609 v (THead k u1 x) (THead k u2 t))) (\lambda (_: (eq T u2 u2)).(or4_intro1 (eq
610 T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead
611 k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v
612 (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t))
613 (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
614 T).(subst0 i0 v (THead k u1 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5
615 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (H6: (ex2 T (\lambda (t3:
616 T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3)))).(ex2_ind T
617 (\lambda (t3: T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3))
618 (or4 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0
619 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3)))
620 (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x)
621 (THead k u2 t))) (\lambda (x0: T).(\lambda (_: (subst0 i0 v u2 x0)).(\lambda
622 (_: (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x))
623 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
624 T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1
625 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)) (ex_intro2 T (\lambda (t3:
626 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1
627 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5 u2) (subst0_fst v u2 u1 i0
628 H0 x k)))))) H6)) (\lambda (_: (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead
629 k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t)
630 t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v (THead k
631 u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)) (ex_intro2
632 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0
633 i0 v (THead k u1 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5 u2)
634 (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (_: (subst0 i0 v u2
635 u2)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3:
636 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1
637 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1
638 x) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t)
639 t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3)) (THead k u2 x)
640 (subst0_snd k v x t i0 H5 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (H1 u2 H0))
641 t2 H4)))) H3)) (\lambda (H3: (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq
642 T t2 (THead k u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1
643 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i0) v t
644 t3))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead k u3
645 t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_:
646 T).(\lambda (t3: T).(subst0 (s k i0) v t t3))) (or4 (eq T (THead k u2 t) t2)
647 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
648 T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2
649 (THead k u2 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t2
650 (THead k x0 x1))).(\lambda (H5: (subst0 i0 v u1 x0)).(\lambda (H6: (subst0 (s
651 k i0) v t x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(or4 (eq T (THead
652 k u2 t) t3) (ex2 T (\lambda (t4: T).(subst0 i0 v (THead k u2 t) t4)) (\lambda
653 (t4: T).(subst0 i0 v t3 t4))) (subst0 i0 v (THead k u2 t) t3) (subst0 i0 v t3
654 (THead k u2 t)))) (or4_ind (eq T u2 x0) (ex2 T (\lambda (t3: T).(subst0 i0 v
655 u2 t3)) (\lambda (t3: T).(subst0 i0 v x0 t3))) (subst0 i0 v u2 x0) (subst0 i0
656 v x0 u2) (or4 (eq T (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3:
657 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0
658 x1) t3))) (subst0 i0 v (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k
659 x0 x1) (THead k u2 t))) (\lambda (H7: (eq T u2 x0)).(eq_ind_r T x0 (\lambda
660 (t3: T).(or4 (eq T (THead k t3 t) (THead k x0 x1)) (ex2 T (\lambda (t4:
661 T).(subst0 i0 v (THead k t3 t) t4)) (\lambda (t4: T).(subst0 i0 v (THead k x0
662 x1) t4))) (subst0 i0 v (THead k t3 t) (THead k x0 x1)) (subst0 i0 v (THead k
663 x0 x1) (THead k t3 t)))) (or4_intro2 (eq T (THead k x0 t) (THead k x0 x1))
664 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k x0 t) t3)) (\lambda (t3:
665 T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k x0 t) (THead k x0
666 x1)) (subst0 i0 v (THead k x0 x1) (THead k x0 t)) (subst0_snd k v x1 t i0 H6
667 x0)) u2 H7)) (\lambda (H7: (ex2 T (\lambda (t3: T).(subst0 i0 v u2 t3))
668 (\lambda (t3: T).(subst0 i0 v x0 t3)))).(ex2_ind T (\lambda (t3: T).(subst0
669 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v x0 t3)) (or4 (eq T (THead k u2 t)
670 (THead k x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
671 (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k u2
672 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t))) (\lambda
673 (x: T).(\lambda (H8: (subst0 i0 v u2 x)).(\lambda (H9: (subst0 i0 v x0
674 x)).(or4_intro1 (eq T (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3:
675 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0
676 x1) t3))) (subst0 i0 v (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k
677 x0 x1) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2
678 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3)) (THead k x x1)
679 (subst0_both v u2 x i0 H8 k t x1 H6) (subst0_fst v x x0 i0 H9 x1 k)))))) H7))
680 (\lambda (H7: (subst0 i0 v u2 x0)).(or4_intro2 (eq T (THead k u2 t) (THead k
681 x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda
682 (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k u2 t) (THead
683 k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t)) (subst0_both v u2 x0
684 i0 H7 k t x1 H6))) (\lambda (H7: (subst0 i0 v x0 u2)).(or4_intro1 (eq T
685 (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
686 u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v
687 (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t))
688 (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
689 T).(subst0 i0 v (THead k x0 x1) t3)) (THead k u2 x1) (subst0_snd k v x1 t i0
690 H6 u2) (subst0_fst v u2 x0 i0 H7 x1 k)))) (H1 x0 H5)) t2 H4)))))) H3))
691 (subst0_gen_head k v u1 t t2 i0 H2)))))))))))) (\lambda (k: K).(\lambda (v:
692 T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (H0: (subst0
693 (s k i0) v t3 t2)).(\lambda (H1: ((\forall (t4: T).((subst0 (s k i0) v t3 t4)
694 \to (or4 (eq T t2 t4) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
695 (\lambda (t: T).(subst0 (s k i0) v t4 t))) (subst0 (s k i0) v t2 t4) (subst0
696 (s k i0) v t4 t2)))))).(\lambda (u0: T).(\lambda (t4: T).(\lambda (H2:
697 (subst0 i0 v (THead k u0 t3) t4)).(or3_ind (ex2 T (\lambda (u2: T).(eq T t4
698 (THead k u2 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2))) (ex2 T (\lambda (t5:
699 T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i0) v t3 t5)))
700 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead k u2 t5))))
701 (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_:
702 T).(\lambda (t5: T).(subst0 (s k i0) v t3 t5)))) (or4 (eq T (THead k u0 t2)
703 t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
704 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2) t4) (subst0 i0 v t4
705 (THead k u0 t2))) (\lambda (H3: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2
706 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2)))).(ex2_ind T (\lambda (u2: T).(eq
707 T t4 (THead k u2 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2)) (or4 (eq T
708 (THead k u0 t2) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
709 (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2) t4) (subst0
710 i0 v t4 (THead k u0 t2))) (\lambda (x: T).(\lambda (H4: (eq T t4 (THead k x
711 t3))).(\lambda (H5: (subst0 i0 v u0 x)).(eq_ind_r T (THead k x t3) (\lambda
712 (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T (\lambda (t5: T).(subst0 i0 v
713 (THead k u0 t2) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
714 (THead k u0 t2) t) (subst0 i0 v t (THead k u0 t2)))) (or4_ind (eq T t2 t2)
715 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k
716 i0) v t2 t))) (subst0 (s k i0) v t2 t2) (subst0 (s k i0) v t2 t2) (or4 (eq T
717 (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
718 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v
719 (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)))
720 (\lambda (_: (eq T t2 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3))
721 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
722 T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x
723 t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
724 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
725 t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3
726 i0 H0 x)))) (\lambda (H6: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
727 (\lambda (t: T).(subst0 (s k i0) v t2 t)))).(ex2_ind T (\lambda (t:
728 T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k i0) v t2 t)) (or4
729 (eq T (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v
730 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0
731 i0 v (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0
732 t2))) (\lambda (x0: T).(\lambda (_: (subst0 (s k i0) v t2 x0)).(\lambda (_:
733 (subst0 (s k i0) v t2 x0)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3))
734 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
735 T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x
736 t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
737 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
738 t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3
739 i0 H0 x)))))) H6)) (\lambda (_: (subst0 (s k i0) v t2 t2)).(or4_intro1 (eq T
740 (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
741 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v
742 (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2))
743 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
744 T).(subst0 i0 v (THead k x t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2
745 k) (subst0_snd k v t2 t3 i0 H0 x)))) (\lambda (_: (subst0 (s k i0) v t2
746 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t:
747 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
748 t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x
749 t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0
750 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (THead k x t2)
751 (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3 i0 H0 x)))) (H1 t2 H0))
752 t4 H4)))) H3)) (\lambda (H3: (ex2 T (\lambda (t5: T).(eq T t4 (THead k u0
753 t5))) (\lambda (t5: T).(subst0 (s k i0) v t3 t5)))).(ex2_ind T (\lambda (t5:
754 T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i0) v t3 t5))
755 (or4 (eq T (THead k u0 t2) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
756 u0 t2) t)) (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2)
757 t4) (subst0 i0 v t4 (THead k u0 t2))) (\lambda (x: T).(\lambda (H4: (eq T t4
758 (THead k u0 x))).(\lambda (H5: (subst0 (s k i0) v t3 x)).(eq_ind_r T (THead k
759 u0 x) (\lambda (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T (\lambda (t5:
760 T).(subst0 i0 v (THead k u0 t2) t5)) (\lambda (t5: T).(subst0 i0 v t t5)))
761 (subst0 i0 v (THead k u0 t2) t) (subst0 i0 v t (THead k u0 t2)))) (or4_ind
762 (eq T t2 x) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t:
763 T).(subst0 (s k i0) v x t))) (subst0 (s k i0) v t2 x) (subst0 (s k i0) v x
764 t2) (or4 (eq T (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0
765 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)))
766 (subst0 i0 v (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0 x)
767 (THead k u0 t2))) (\lambda (H6: (eq T t2 x)).(eq_ind_r T x (\lambda (t:
768 T).(or4 (eq T (THead k u0 t) (THead k u0 x)) (ex2 T (\lambda (t5: T).(subst0
769 i0 v (THead k u0 t) t5)) (\lambda (t5: T).(subst0 i0 v (THead k u0 x) t5)))
770 (subst0 i0 v (THead k u0 t) (THead k u0 x)) (subst0 i0 v (THead k u0 x)
771 (THead k u0 t)))) (or4_intro0 (eq T (THead k u0 x) (THead k u0 x)) (ex2 T
772 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)) (\lambda (t: T).(subst0 i0 v
773 (THead k u0 x) t))) (subst0 i0 v (THead k u0 x) (THead k u0 x)) (subst0 i0 v
774 (THead k u0 x) (THead k u0 x)) (refl_equal T (THead k u0 x))) t2 H6))
775 (\lambda (H6: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t:
776 T).(subst0 (s k i0) v x t)))).(ex2_ind T (\lambda (t: T).(subst0 (s k i0) v
777 t2 t)) (\lambda (t: T).(subst0 (s k i0) v x t)) (or4 (eq T (THead k u0 t2)
778 (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
779 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v (THead k u0 t2)
780 (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2))) (\lambda (x0:
781 T).(\lambda (H7: (subst0 (s k i0) v t2 x0)).(\lambda (H8: (subst0 (s k i0) v
782 x x0)).(or4_intro1 (eq T (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t:
783 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0
784 x) t))) (subst0 i0 v (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0
785 x) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2)
786 t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)) (THead k u0 x0)
787 (subst0_snd k v x0 t2 i0 H7 u0) (subst0_snd k v x0 x i0 H8 u0)))))) H6))
788 (\lambda (H6: (subst0 (s k i0) v t2 x)).(or4_intro2 (eq T (THead k u0 t2)
789 (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
790 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v (THead k u0 t2)
791 (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2)) (subst0_snd k v
792 x t2 i0 H6 u0))) (\lambda (H6: (subst0 (s k i0) v x t2)).(or4_intro3 (eq T
793 (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
794 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v
795 (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2))
796 (subst0_snd k v t2 x i0 H6 u0))) (H1 x H5)) t4 H4)))) H3)) (\lambda (H3:
797 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead k u2 t5))))
798 (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_:
799 T).(\lambda (t5: T).(subst0 (s k i0) v t3 t5))))).(ex3_2_ind T T (\lambda
800 (u2: T).(\lambda (t5: T).(eq T t4 (THead k u2 t5)))) (\lambda (u2:
801 T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_: T).(\lambda (t5:
802 T).(subst0 (s k i0) v t3 t5))) (or4 (eq T (THead k u0 t2) t4) (ex2 T (\lambda
803 (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v t4 t)))
804 (subst0 i0 v (THead k u0 t2) t4) (subst0 i0 v t4 (THead k u0 t2))) (\lambda
805 (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t4 (THead k x0 x1))).(\lambda
806 (H5: (subst0 i0 v u0 x0)).(\lambda (H6: (subst0 (s k i0) v t3 x1)).(eq_ind_r
807 T (THead k x0 x1) (\lambda (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T
808 (\lambda (t5: T).(subst0 i0 v (THead k u0 t2) t5)) (\lambda (t5: T).(subst0
809 i0 v t t5))) (subst0 i0 v (THead k u0 t2) t) (subst0 i0 v t (THead k u0
810 t2)))) (or4_ind (eq T t2 x1) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
811 (\lambda (t: T).(subst0 (s k i0) v x1 t))) (subst0 (s k i0) v t2 x1) (subst0
812 (s k i0) v x1 t2) (or4 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda
813 (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k
814 x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead
815 k x0 x1) (THead k u0 t2))) (\lambda (H7: (eq T t2 x1)).(eq_ind_r T x1
816 (\lambda (t: T).(or4 (eq T (THead k u0 t) (THead k x0 x1)) (ex2 T (\lambda
817 (t5: T).(subst0 i0 v (THead k u0 t) t5)) (\lambda (t5: T).(subst0 i0 v (THead
818 k x0 x1) t5))) (subst0 i0 v (THead k u0 t) (THead k x0 x1)) (subst0 i0 v
819 (THead k x0 x1) (THead k u0 t)))) (or4_intro2 (eq T (THead k u0 x1) (THead k
820 x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 x1) t)) (\lambda (t:
821 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u0 x1) (THead k x0
822 x1)) (subst0 i0 v (THead k x0 x1) (THead k u0 x1)) (subst0_fst v x0 u0 i0 H5
823 x1 k)) t2 H7)) (\lambda (H7: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
824 (\lambda (t: T).(subst0 (s k i0) v x1 t)))).(ex2_ind T (\lambda (t:
825 T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)) (or4
826 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
827 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
828 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
829 u0 t2))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i0) v t2 x)).(\lambda
830 (H9: (subst0 (s k i0) v x1 x)).(or4_intro1 (eq T (THead k u0 t2) (THead k x0
831 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
832 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0
833 x1)) (subst0 i0 v (THead k x0 x1) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
834 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
835 x1) t)) (THead k x0 x) (subst0_both v u0 x0 i0 H5 k t2 x H8) (subst0_snd k v
836 x x1 i0 H9 x0)))))) H7)) (\lambda (H7: (subst0 (s k i0) v t2 x1)).(or4_intro2
837 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
838 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
839 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
840 u0 t2)) (subst0_both v u0 x0 i0 H5 k t2 x1 H7))) (\lambda (H7: (subst0 (s k
841 i0) v x1 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T
842 (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v
843 (THead k x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0
844 v (THead k x0 x1) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
845 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k
846 x0 t2) (subst0_fst v x0 u0 i0 H5 t2 k) (subst0_snd k v t2 x1 i0 H7 x0)))) (H1
847 x1 H6)) t4 H4)))))) H3)) (subst0_gen_head k v u0 t3 t4 i0 H2))))))))))))
848 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda
849 (H0: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (t2: T).((subst0 i0 v u1
850 t2) \to (or4 (eq T u2 t2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda
851 (t: T).(subst0 i0 v t2 t))) (subst0 i0 v u2 t2) (subst0 i0 v t2
852 u2)))))).(\lambda (k: K).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2:
853 (subst0 (s k i0) v t2 t3)).(\lambda (H3: ((\forall (t4: T).((subst0 (s k i0)
854 v t2 t4) \to (or4 (eq T t3 t4) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3
855 t)) (\lambda (t: T).(subst0 (s k i0) v t4 t))) (subst0 (s k i0) v t3 t4)
856 (subst0 (s k i0) v t4 t3)))))).(\lambda (t4: T).(\lambda (H4: (subst0 i0 v
857 (THead k u1 t2) t4)).(or3_ind (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3
858 t2))) (\lambda (u3: T).(subst0 i0 v u1 u3))) (ex2 T (\lambda (t5: T).(eq T t4
859 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i0) v t2 t5))) (ex3_2 T T
860 (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3:
861 T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_: T).(\lambda (t5:
862 T).(subst0 (s k i0) v t2 t5)))) (or4 (eq T (THead k u2 t3) t4) (ex2 T
863 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
864 t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4 (THead k u2 t3)))
865 (\lambda (H5: (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3 t2))) (\lambda
866 (u3: T).(subst0 i0 v u1 u3)))).(ex2_ind T (\lambda (u3: T).(eq T t4 (THead k
867 u3 t2))) (\lambda (u3: T).(subst0 i0 v u1 u3)) (or4 (eq T (THead k u2 t3) t4)
868 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
869 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4
870 (THead k u2 t3))) (\lambda (x: T).(\lambda (H6: (eq T t4 (THead k x
871 t2))).(\lambda (H7: (subst0 i0 v u1 x)).(eq_ind_r T (THead k x t2) (\lambda
872 (t: T).(or4 (eq T (THead k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0 i0 v
873 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
874 (THead k u2 t3) t) (subst0 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 t3)
875 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k
876 i0) v t3 t))) (subst0 (s k i0) v t3 t3) (subst0 (s k i0) v t3 t3) (or4 (eq T
877 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
878 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
879 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)))
880 (\lambda (_: (eq T t3 t3)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t:
881 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x)
882 (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
883 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
884 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
885 x t2) (THead k u2 t3))) (\lambda (H9: (eq T u2 x)).(eq_ind_r T x (\lambda (t:
886 T).(or4 (eq T (THead k t t3) (THead k x t2)) (ex2 T (\lambda (t5: T).(subst0
887 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x t2) t5)))
888 (subst0 i0 v (THead k t t3) (THead k x t2)) (subst0 i0 v (THead k x t2)
889 (THead k t t3)))) (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T
890 (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v
891 (THead k x t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v
892 (THead k x t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H9))
893 (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
894 T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
895 (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2))
896 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
897 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
898 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x0: T).(\lambda
899 (H10: (subst0 i0 v u2 x0)).(\lambda (H11: (subst0 i0 v x x0)).(or4_intro1 (eq
900 T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
901 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
902 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
903 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
904 T).(subst0 i0 v (THead k x t2) t)) (THead k x0 t3) (subst0_fst v x0 u2 i0 H10
905 t3 k) (subst0_both v x x0 i0 H11 k t2 t3 H2)))))) H9)) (\lambda (H9: (subst0
906 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
907 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
908 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
909 x t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
910 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x t3)
911 (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd k v t3 t2 i0 H2 x)))) (\lambda
912 (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k x t2))
913 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
914 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
915 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H9 k
916 t2 t3 H2))) (H1 x H7))) (\lambda (H8: (ex2 T (\lambda (t: T).(subst0 (s k i0)
917 v t3 t)) (\lambda (t: T).(subst0 (s k i0) v t3 t)))).(ex2_ind T (\lambda (t:
918 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v t3 t)) (or4
919 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v
920 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0
921 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2
922 t3))) (\lambda (x0: T).(\lambda (_: (subst0 (s k i0) v t3 x0)).(\lambda (_:
923 (subst0 (s k i0) v t3 x0)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t:
924 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x)
925 (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
926 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
927 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
928 x t2) (THead k u2 t3))) (\lambda (H11: (eq T u2 x)).(eq_ind_r T x (\lambda
929 (t: T).(or4 (eq T (THead k t t3) (THead k x t2)) (ex2 T (\lambda (t5:
930 T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x
931 t2) t5))) (subst0 i0 v (THead k t t3) (THead k x t2)) (subst0 i0 v (THead k x
932 t2) (THead k t t3)))) (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T
933 (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v
934 (THead k x t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v
935 (THead k x t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H11))
936 (\lambda (H11: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
937 T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
938 (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2))
939 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
940 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
941 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x1: T).(\lambda
942 (H12: (subst0 i0 v u2 x1)).(\lambda (H13: (subst0 i0 v x x1)).(or4_intro1 (eq
943 T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
944 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
945 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
946 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
947 T).(subst0 i0 v (THead k x t2) t)) (THead k x1 t3) (subst0_fst v x1 u2 i0 H12
948 t3 k) (subst0_both v x x1 i0 H13 k t2 t3 H2)))))) H11)) (\lambda (H11:
949 (subst0 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T
950 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
951 (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v
952 (THead k x t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
953 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k
954 x t3) (subst0_fst v x u2 i0 H11 t3 k) (subst0_snd k v t3 t2 i0 H2 x))))
955 (\lambda (H11: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k
956 x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
957 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
958 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H11
959 k t2 t3 H2))) (H1 x H7))))) H8)) (\lambda (_: (subst0 (s k i0) v t3
960 t3)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda
961 (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x) (subst0 i0 v x u2) (or4 (eq T
962 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
963 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
964 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)))
965 (\lambda (H9: (eq T u2 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k
966 t t3) (THead k x t2)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3)
967 t5)) (\lambda (t5: T).(subst0 i0 v (THead k x t2) t5))) (subst0 i0 v (THead k
968 t t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k t t3))))
969 (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T (\lambda (t:
970 T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
971 t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v (THead k x
972 t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H9)) (\lambda (H9:
973 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x
974 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0
975 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
976 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
977 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
978 t2) (THead k u2 t3))) (\lambda (x0: T).(\lambda (H10: (subst0 i0 v u2
979 x0)).(\lambda (H11: (subst0 i0 v x x0)).(or4_intro1 (eq T (THead k u2 t3)
980 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
981 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
982 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (ex_intro2 T
983 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
984 (THead k x t2) t)) (THead k x0 t3) (subst0_fst v x0 u2 i0 H10 t3 k)
985 (subst0_both v x x0 i0 H11 k t2 t3 H2)))))) H9)) (\lambda (H9: (subst0 i0 v
986 u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
987 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
988 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
989 t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
990 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x t3)
991 (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd k v t3 t2 i0 H2 x)))) (\lambda
992 (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k x t2))
993 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
994 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
995 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H9 k
996 t2 t3 H2))) (H1 x H7))) (\lambda (_: (subst0 (s k i0) v t3 t3)).(or4_ind (eq
997 T u2 x) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0
998 v x t))) (subst0 i0 v u2 x) (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3)
999 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1000 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
1001 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (H9:
1002 (eq T u2 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k t t3) (THead k
1003 x t2)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5:
1004 T).(subst0 i0 v (THead k x t2) t5))) (subst0 i0 v (THead k t t3) (THead k x
1005 t2)) (subst0 i0 v (THead k x t2) (THead k t t3)))) (or4_intro3 (eq T (THead k
1006 x t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k x t3) t))
1007 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k x t3)
1008 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k x t3)) (subst0_snd k v
1009 t3 t2 i0 H2 x)) u2 H9)) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2
1010 t)) (\lambda (t: T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0
1011 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3)
1012 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1013 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
1014 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x0:
1015 T).(\lambda (H10: (subst0 i0 v u2 x0)).(\lambda (H11: (subst0 i0 v x
1016 x0)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
1017 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
1018 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
1019 t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
1020 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x0 t3)
1021 (subst0_fst v x0 u2 i0 H10 t3 k) (subst0_both v x x0 i0 H11 k t2 t3 H2))))))
1022 H9)) (\lambda (H9: (subst0 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3)
1023 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1024 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
1025 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (ex_intro2 T
1026 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1027 (THead k x t2) t)) (THead k x t3) (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd
1028 k v t3 t2 i0 H2 x)))) (\lambda (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T
1029 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1030 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
1031 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
1032 (subst0_both v x u2 i0 H9 k t2 t3 H2))) (H1 x H7))) (H3 t3 H2)) t4 H6))))
1033 H5)) (\lambda (H5: (ex2 T (\lambda (t5: T).(eq T t4 (THead k u1 t5)))
1034 (\lambda (t5: T).(subst0 (s k i0) v t2 t5)))).(ex2_ind T (\lambda (t5: T).(eq
1035 T t4 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i0) v t2 t5)) (or4 (eq T
1036 (THead k u2 t3) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1037 (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0
1038 i0 v t4 (THead k u2 t3))) (\lambda (x: T).(\lambda (H6: (eq T t4 (THead k u1
1039 x))).(\lambda (H7: (subst0 (s k i0) v t2 x)).(eq_ind_r T (THead k u1 x)
1040 (\lambda (t: T).(or4 (eq T (THead k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0
1041 i0 v (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
1042 (THead k u2 t3) t) (subst0 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 x)
1043 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k
1044 i0) v x t))) (subst0 (s k i0) v t3 x) (subst0 (s k i0) v x t3) (or4 (eq T
1045 (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1046 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1047 (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)))
1048 (\lambda (H8: (eq T t3 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k
1049 u2 t) (THead k u1 x)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t)
1050 t5)) (\lambda (t5: T).(subst0 i0 v (THead k u1 x) t5))) (subst0 i0 v (THead k
1051 u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)))) (or4_ind
1052 (eq T u2 u2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1053 T).(subst0 i0 v u2 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T
1054 (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1055 u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1056 (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x)))
1057 (\lambda (_: (eq T u2 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x))
1058 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t:
1059 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1
1060 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x
1061 k))) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1062 T).(subst0 i0 v u2 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1063 (\lambda (t: T).(subst0 i0 v u2 t)) (or4 (eq T (THead k u2 x) (THead k u1 x))
1064 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t:
1065 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1
1066 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x))) (\lambda (x0: T).(\lambda
1067 (_: (subst0 i0 v u2 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro3 (eq T
1068 (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1069 u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1070 (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x))
1071 (subst0_fst v u2 u1 i0 H0 x k))))) H9)) (\lambda (_: (subst0 i0 v u2
1072 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t:
1073 T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1074 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1
1075 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x k))) (\lambda (_: (subst0 i0 v
1076 u2 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t:
1077 T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1078 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1
1079 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x k))) (H1 u2 H0)) t3 H8))
1080 (\lambda (H8: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t:
1081 T).(subst0 (s k i0) v x t)))).(ex2_ind T (\lambda (t: T).(subst0 (s k i0) v
1082 t3 t)) (\lambda (t: T).(subst0 (s k i0) v x t)) (or4 (eq T (THead k u2 t3)
1083 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1084 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1085 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (x0:
1086 T).(\lambda (H9: (subst0 (s k i0) v t3 x0)).(\lambda (H10: (subst0 (s k i0) v
1087 x x0)).(or4_ind (eq T u2 u2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t))
1088 (\lambda (t: T).(subst0 i0 v u2 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2)
1089 (or4 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0
1090 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)))
1091 (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x)
1092 (THead k u2 t3))) (\lambda (_: (eq T u2 u2)).(or4_intro1 (eq T (THead k u2
1093 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1094 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1095 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (ex_intro2 T
1096 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1097 (THead k u1 x) t)) (THead k u2 x0) (subst0_snd k v x0 t3 i0 H9 u2)
1098 (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (\lambda (H11: (ex2 T (\lambda (t:
1099 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)))).(ex2_ind T
1100 (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)) (or4
1101 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v
1102 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0
1103 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2
1104 t3))) (\lambda (x1: T).(\lambda (_: (subst0 i0 v u2 x1)).(\lambda (_: (subst0
1105 i0 v u2 x1)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1106 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1107 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1108 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1109 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1110 u2 x0) (subst0_snd k v x0 t3 i0 H9 u2) (subst0_both v u1 u2 i0 H0 k x x0
1111 H10)))))) H11)) (\lambda (_: (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead k
1112 u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1113 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2
1114 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (ex_intro2 T
1115 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1116 (THead k u1 x) t)) (THead k u2 x0) (subst0_snd k v x0 t3 i0 H9 u2)
1117 (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (\lambda (_: (subst0 i0 v u2
1118 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1119 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1120 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1121 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1122 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x0)
1123 (subst0_snd k v x0 t3 i0 H9 u2) (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (H1
1124 u2 H0))))) H8)) (\lambda (H8: (subst0 (s k i0) v t3 x)).(or4_ind (eq T u2 u2)
1125 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2
1126 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t3)
1127 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1128 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1129 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (_:
1130 (eq T u2 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1131 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1132 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1133 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1134 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1135 u2 x) (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k))))
1136 (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1137 T).(subst0 i0 v u2 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1138 (\lambda (t: T).(subst0 i0 v u2 t)) (or4 (eq T (THead k u2 t3) (THead k u1
1139 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1140 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1
1141 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (x0: T).(\lambda
1142 (_: (subst0 i0 v u2 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro1 (eq T
1143 (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1144 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1145 (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))
1146 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1147 T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x) (subst0_snd k v x t3 i0 H8
1148 u2) (subst0_fst v u2 u1 i0 H0 x k)))))) H9)) (\lambda (_: (subst0 i0 v u2
1149 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1150 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1151 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1152 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1153 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x)
1154 (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (_:
1155 (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1156 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1157 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1158 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1159 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1160 u2 x) (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (H1 u2
1161 H0))) (\lambda (H8: (subst0 (s k i0) v x t3)).(or4_ind (eq T u2 u2) (ex2 T
1162 (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)))
1163 (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t3) (THead k
1164 u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1165 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1
1166 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (_: (eq T u2
1167 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1168 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1169 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1170 x) (THead k u2 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (\lambda (H9:
1171 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2
1172 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0
1173 i0 v u2 t)) (or4 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1174 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1175 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1176 x) (THead k u2 t3))) (\lambda (x0: T).(\lambda (_: (subst0 i0 v u2
1177 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro3 (eq T (THead k u2 t3)
1178 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1179 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1180 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (subst0_both v
1181 u1 u2 i0 H0 k x t3 H8))))) H9)) (\lambda (_: (subst0 i0 v u2 u2)).(or4_intro3
1182 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v
1183 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0
1184 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2
1185 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (\lambda (_: (subst0 i0 v u2
1186 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1187 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1188 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1189 x) (THead k u2 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (H1 u2 H0))) (H3
1190 x H7)) t4 H6)))) H5)) (\lambda (H5: (ex3_2 T T (\lambda (u3: T).(\lambda (t5:
1191 T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v
1192 u1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i0) v t2
1193 t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3
1194 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_:
1195 T).(\lambda (t5: T).(subst0 (s k i0) v t2 t5))) (or4 (eq T (THead k u2 t3)
1196 t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1197 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4
1198 (THead k u2 t3))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H6: (eq T t4
1199 (THead k x0 x1))).(\lambda (H7: (subst0 i0 v u1 x0)).(\lambda (H8: (subst0 (s
1200 k i0) v t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(or4 (eq T (THead
1201 k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t3) t5))
1202 (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v (THead k u2 t3) t) (subst0
1203 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 x1) (ex2 T (\lambda (t:
1204 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)))
1205 (subst0 (s k i0) v t3 x1) (subst0 (s k i0) v x1 t3) (or4 (eq T (THead k u2
1206 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1207 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1208 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1209 (H9: (eq T t3 x1)).(eq_ind_r T x1 (\lambda (t: T).(or4 (eq T (THead k u2 t)
1210 (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t) t5))
1211 (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v (THead k u2
1212 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t)))) (or4_ind
1213 (eq T u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1214 T).(subst0 i0 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2) (or4 (eq T
1215 (THead k u2 x1) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1216 u2 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v
1217 (THead k u2 x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2
1218 x1))) (\lambda (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t: T).(or4 (eq T
1219 (THead k t x1) (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k
1220 t x1) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v
1221 (THead k t x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k t
1222 x1)))) (or4_intro0 (eq T (THead k x0 x1) (THead k x0 x1)) (ex2 T (\lambda (t:
1223 T).(subst0 i0 v (THead k x0 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1224 x1) t))) (subst0 i0 v (THead k x0 x1) (THead k x0 x1)) (subst0 i0 v (THead k
1225 x0 x1) (THead k x0 x1)) (refl_equal T (THead k x0 x1))) u2 H10)) (\lambda
1226 (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v
1227 x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1228 T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2 T
1229 (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0 v
1230 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0 i0
1231 v (THead k x0 x1) (THead k u2 x1))) (\lambda (x: T).(\lambda (H11: (subst0 i0
1232 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq T (THead k u2 x1)
1233 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t))
1234 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1235 x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 x1)) (ex_intro2
1236 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0
1237 v (THead k x0 x1) t)) (THead k x x1) (subst0_fst v x u2 i0 H11 x1 k)
1238 (subst0_fst v x x0 i0 H12 x1 k)))))) H10)) (\lambda (H10: (subst0 i0 v u2
1239 x0)).(or4_intro2 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2 T (\lambda (t:
1240 T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1241 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0 i0 v (THead k
1242 x0 x1) (THead k u2 x1)) (subst0_fst v x0 u2 i0 H10 x1 k))) (\lambda (H10:
1243 (subst0 i0 v x0 u2)).(or4_intro3 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2
1244 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0
1245 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0
1246 i0 v (THead k x0 x1) (THead k u2 x1)) (subst0_fst v u2 x0 i0 H10 x1 k))) (H1
1247 x0 H7)) t3 H9)) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3
1248 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)))).(ex2_ind T (\lambda (t:
1249 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)) (or4
1250 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
1251 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
1252 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
1253 u2 t3))) (\lambda (x: T).(\lambda (H10: (subst0 (s k i0) v t3 x)).(\lambda
1254 (H11: (subst0 (s k i0) v x1 x)).(or4_ind (eq T u2 x0) (ex2 T (\lambda (t:
1255 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x0 t))) (subst0 i0 v u2
1256 x0) (subst0 i0 v x0 u2) (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T
1257 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1258 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0
1259 v (THead k x0 x1) (THead k u2 t3))) (\lambda (H12: (eq T u2 x0)).(eq_ind_r T
1260 x0 (\lambda (t: T).(or4 (eq T (THead k t t3) (THead k x0 x1)) (ex2 T (\lambda
1261 (t5: T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead
1262 k x0 x1) t5))) (subst0 i0 v (THead k t t3) (THead k x0 x1)) (subst0 i0 v
1263 (THead k x0 x1) (THead k t t3)))) (or4_intro1 (eq T (THead k x0 t3) (THead k
1264 x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t:
1265 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0
1266 x1)) (subst0 i0 v (THead k x0 x1) (THead k x0 t3)) (ex_intro2 T (\lambda (t:
1267 T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1268 x1) t)) (THead k x0 x) (subst0_snd k v x t3 i0 H10 x0) (subst0_snd k v x x1
1269 i0 H11 x0))) u2 H12)) (\lambda (H12: (ex2 T (\lambda (t: T).(subst0 i0 v u2
1270 t)) (\lambda (t: T).(subst0 i0 v x0 t)))).(ex2_ind T (\lambda (t: T).(subst0
1271 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3)
1272 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1273 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1274 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1275 (x2: T).(\lambda (H13: (subst0 i0 v u2 x2)).(\lambda (H14: (subst0 i0 v x0
1276 x2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1277 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1278 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1279 x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
1280 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k x2 x)
1281 (subst0_both v u2 x2 i0 H13 k t3 x H10) (subst0_both v x0 x2 i0 H14 k x1 x
1282 H11)))))) H12)) (\lambda (H12: (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead
1283 k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1284 t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k
1285 u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))
1286 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1287 T).(subst0 i0 v (THead k x0 x1) t)) (THead k x0 x) (subst0_both v u2 x0 i0
1288 H12 k t3 x H10) (subst0_snd k v x x1 i0 H11 x0)))) (\lambda (H12: (subst0 i0
1289 v x0 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda
1290 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
1291 x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead
1292 k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k
1293 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k u2 x)
1294 (subst0_snd k v x t3 i0 H10 u2) (subst0_both v x0 u2 i0 H12 k x1 x H11))))
1295 (H1 x0 H7))))) H9)) (\lambda (H9: (subst0 (s k i0) v t3 x1)).(or4_ind (eq T
1296 u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0
1297 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2) (or4 (eq T (THead k u2 t3)
1298 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1299 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1300 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1301 (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t: T).(or4 (eq T (THead k t t3)
1302 (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3) t5))
1303 (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v (THead k t
1304 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k t t3))))
1305 (or4_intro2 (eq T (THead k x0 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1306 T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1307 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1308 x0 x1) (THead k x0 t3)) (subst0_snd k v x1 t3 i0 H9 x0)) u2 H10)) (\lambda
1309 (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v
1310 x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1311 T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T
1312 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1313 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0
1314 v (THead k x0 x1) (THead k u2 t3))) (\lambda (x: T).(\lambda (H11: (subst0 i0
1315 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq T (THead k u2 t3)
1316 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1317 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1318 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2
1319 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0
1320 v (THead k x0 x1) t)) (THead k x x1) (subst0_both v u2 x i0 H11 k t3 x1 H9)
1321 (subst0_fst v x x0 i0 H12 x1 k)))))) H10)) (\lambda (H10: (subst0 i0 v u2
1322 x0)).(or4_intro2 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1323 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1324 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1325 x0 x1) (THead k u2 t3)) (subst0_both v u2 x0 i0 H10 k t3 x1 H9))) (\lambda
1326 (H10: (subst0 i0 v x0 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1))
1327 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1328 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0
1329 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t:
1330 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1331 x1) t)) (THead k u2 x1) (subst0_snd k v x1 t3 i0 H9 u2) (subst0_fst v u2 x0
1332 i0 H10 x1 k)))) (H1 x0 H7))) (\lambda (H9: (subst0 (s k i0) v x1
1333 t3)).(or4_ind (eq T u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t))
1334 (\lambda (t: T).(subst0 i0 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2)
1335 (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0
1336 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)))
1337 (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1)
1338 (THead k u2 t3))) (\lambda (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t:
1339 T).(or4 (eq T (THead k t t3) (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0
1340 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5)))
1341 (subst0 i0 v (THead k t t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1)
1342 (THead k t t3)))) (or4_intro3 (eq T (THead k x0 t3) (THead k x0 x1)) (ex2 T
1343 (\lambda (t: T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v
1344 (THead k x0 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0 x1)) (subst0 i0
1345 v (THead k x0 x1) (THead k x0 t3)) (subst0_snd k v t3 x1 i0 H9 x0)) u2 H10))
1346 (\lambda (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1347 T).(subst0 i0 v x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1348 (\lambda (t: T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3) (THead k x0
1349 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1350 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0
1351 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda (x: T).(\lambda
1352 (H11: (subst0 i0 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq
1353 T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
1354 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v
1355 (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2
1356 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda
1357 (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k x t3) (subst0_fst v x u2 i0
1358 H11 t3 k) (subst0_both v x0 x i0 H12 k x1 t3 H9)))))) H10)) (\lambda (H10:
1359 (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2
1360 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0
1361 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0
1362 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0
1363 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead
1364 k x0 t3) (subst0_fst v x0 u2 i0 H10 t3 k) (subst0_snd k v t3 x1 i0 H9 x0))))
1365 (\lambda (H10: (subst0 i0 v x0 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead
1366 k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda
1367 (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead
1368 k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (subst0_both v x0 u2
1369 i0 H10 k x1 t3 H9))) (H1 x0 H7))) (H3 x1 H8)) t4 H6)))))) H5))
1370 (subst0_gen_head k v u1 t2 t4 i0 H4))))))))))))))) i u t0 t1 H))))).
1372 Initial nodes: 25595
1375 theorem subst0_confluence_lift:
1376 \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0
1377 i u t0 (lift (S O) i t1)) \to (\forall (t2: T).((subst0 i u t0 (lift (S O) i
1378 t2)) \to (eq T t1 t2)))))))
1380 \lambda (t0: T).(\lambda (t1: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
1381 (H: (subst0 i u t0 (lift (S O) i t1))).(\lambda (t2: T).(\lambda (H0: (subst0
1382 i u t0 (lift (S O) i t2))).(or4_ind (eq T (lift (S O) i t2) (lift (S O) i
1383 t1)) (ex2 T (\lambda (t: T).(subst0 i u (lift (S O) i t2) t)) (\lambda (t:
1384 T).(subst0 i u (lift (S O) i t1) t))) (subst0 i u (lift (S O) i t2) (lift (S
1385 O) i t1)) (subst0 i u (lift (S O) i t1) (lift (S O) i t2)) (eq T t1 t2)
1386 (\lambda (H1: (eq T (lift (S O) i t2) (lift (S O) i t1))).(let H2 \def
1387 (sym_eq T (lift (S O) i t2) (lift (S O) i t1) H1) in (lift_inj t1 t2 (S O) i
1388 H2))) (\lambda (H1: (ex2 T (\lambda (t: T).(subst0 i u (lift (S O) i t2) t))
1389 (\lambda (t: T).(subst0 i u (lift (S O) i t1) t)))).(ex2_ind T (\lambda (t:
1390 T).(subst0 i u (lift (S O) i t2) t)) (\lambda (t: T).(subst0 i u (lift (S O)
1391 i t1) t)) (eq T t1 t2) (\lambda (x: T).(\lambda (_: (subst0 i u (lift (S O) i
1392 t2) x)).(\lambda (H3: (subst0 i u (lift (S O) i t1)
1393 x)).(subst0_gen_lift_false t1 u x (S O) i i (le_n i) (eq_ind_r nat (plus (S
1394 O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O))
1395 (plus_sym i (S O))) H3 (eq T t1 t2))))) H1)) (\lambda (H1: (subst0 i u (lift
1396 (S O) i t2) (lift (S O) i t1))).(subst0_gen_lift_false t2 u (lift (S O) i t1)
1397 (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n))
1398 (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2)))
1399 (\lambda (H1: (subst0 i u (lift (S O) i t1) (lift (S O) i
1400 t2))).(subst0_gen_lift_false t1 u (lift (S O) i t2) (S O) i i (le_n i)
1401 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O)
1402 i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2)))
1403 (subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).
projects / helm.git / blob