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