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/Level-1/LambdaDelta/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 (u2: T).(\forall (u: T).(\forall (i0:
42 nat).((subst0 i0 u u2 v) \to (ex2 T (\lambda (t: T).(subst0 i u2 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 (u2:
72 T).(\forall (u: T).(\forall (i0: nat).((subst0 i0 u u2 v) \to (ex2 T (\lambda
73 (t: T).(subst0 i u2 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 (u1: T).(\forall (u:
76 T).(\forall (i0: nat).((subst0 i0 u u1 v) \to (ex2 T (\lambda (t: T).(subst0
77 (s k i) u1 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 (u2: T).(\forall (u: T).(\forall (i0: nat).((subst0 i0 u v u2) \to
118 (ex2 T (\lambda (t: T).(subst0 i u2 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 (u2: T).(\forall (u: T).(\forall (i0:
148 nat).((subst0 i0 u v u2) \to (ex2 T (\lambda (t: T).(subst0 i u2 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 (u1: T).(\forall (u: T).(\forall (i0:
152 nat).((subst0 i0 u v u1) \to (ex2 T (\lambda (t: T).(subst0 (s k i) u1 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 (u2: T).(eq T t3 (THead k u2 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 (t2: T).(eq T t3 (THead k u2 t2))) (\lambda (t2:
201 T).(subst0 (s k i0) v0 t t2)))).(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 (u2: T).(\lambda (t2: T).(eq T
207 t3 (THead k u2 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v0 u2 u3)))
208 (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i0) v0 t t2))))).(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 (t2: T).(eq T t4 (THead k u
233 t2))) (\lambda (t2: T).(subst0 (s k i0) v0 t0 t2)))).(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 (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_:
240 T).(subst0 i0 v0 u u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i0) v0
241 t0 t2))))).(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 (u2: T).(eq T t4 (THead k u2 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 (t2: T).(eq T t4 (THead k u2 t2)))
267 (\lambda (t2: T).(subst0 (s k i0) v0 t3 t2)))).(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 (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u3:
274 T).(\lambda (_: T).(subst0 i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t2:
275 T).(subst0 (s k i0) v0 t3 t2))))).(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 (u2: T).(eq T t2 (THead k u2 t))) (\lambda (u2: T).(subst0 i2 u3 u0
322 u2)))).(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 (t2: T).(subst0 (s k i2) u3 t t2)))).(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 (u2: T).(\lambda (t3: T).(eq
345 T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0
346 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i2) u3 t
347 t2))))).(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 (u2: T).(eq T t4 (THead k u2 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 (t2: T).(eq T t4 (THead k u t2))) (\lambda (t2: T).(subst0 (s k i2)
387 u2 t3 t2)))).(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 (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2))))
402 (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_:
403 T).(\lambda (t2: T).(subst0 (s k i2) u2 t3 t2))))).(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 (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq
427 nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 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 (u2: T).(eq T t4 (THead k u2 t2))) (\lambda
438 (u2: T).(subst0 i2 u3 u0 u2)))).(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 (t2: T).(eq T t4 (THead k u0 t2))) (\lambda (t3: T).(subst0 (s k i2)
452 u3 t2 t3)))).(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 (u2: T).(\lambda (t2: T).(eq T t4
467 (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0 u2)))
468 (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t2 t3))))).(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 (u2: T).(eq T t2 (THead k u2
525 t))) (\lambda (u2: T).(subst0 i0 v u1 u2)))).(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 (t: T).(subst0 i0 v u2 t))
547 (\lambda (t: T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t3: T).(subst0 i0 v
548 u2 t3)) (\lambda (t3: T).(subst0 i0 v x t3)) (or4 (eq T (THead k u2 t) (THead
549 k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda
550 (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t) (THead k
551 x t)) (subst0 i0 v (THead k x t) (THead k u2 t))) (\lambda (x0: T).(\lambda
552 (H7: (subst0 i0 v u2 x0)).(\lambda (H8: (subst0 i0 v x x0)).(or4_intro1 (eq T
553 (THead k u2 t) (THead k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
554 u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v
555 (THead k u2 t) (THead k x t)) (subst0 i0 v (THead k x t) (THead k u2 t))
556 (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
557 T).(subst0 i0 v (THead k x t) t3)) (THead k x0 t) (subst0_fst v x0 u2 i0 H7 t
558 k) (subst0_fst v x0 x i0 H8 t k)))))) H6)) (\lambda (H6: (subst0 i0 v u2
559 x)).(or4_intro2 (eq T (THead k u2 t) (THead k x t)) (ex2 T (\lambda (t3:
560 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x
561 t) t3))) (subst0 i0 v (THead k u2 t) (THead k x t)) (subst0 i0 v (THead k x
562 t) (THead k u2 t)) (subst0_fst v x u2 i0 H6 t k))) (\lambda (H6: (subst0 i0 v
563 x u2)).(or4_intro3 (eq T (THead k u2 t) (THead k x t)) (ex2 T (\lambda (t3:
564 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x
565 t) t3))) (subst0 i0 v (THead k u2 t) (THead k x t)) (subst0 i0 v (THead k x
566 t) (THead k u2 t)) (subst0_fst v u2 x i0 H6 t k))) (H1 x H5)) t2 H4)))) H3))
567 (\lambda (H3: (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda
568 (t2: T).(subst0 (s k i0) v t t2)))).(ex2_ind T (\lambda (t3: T).(eq T t2
569 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i0) v t t3)) (or4 (eq T
570 (THead k u2 t) t2) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
571 (\lambda (t3: T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2)
572 (subst0 i0 v t2 (THead k u2 t))) (\lambda (x: T).(\lambda (H4: (eq T t2
573 (THead k u1 x))).(\lambda (H5: (subst0 (s k i0) v t x)).(eq_ind_r T (THead k
574 u1 x) (\lambda (t3: T).(or4 (eq T (THead k u2 t) t3) (ex2 T (\lambda (t4:
575 T).(subst0 i0 v (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i0 v t3 t4)))
576 (subst0 i0 v (THead k u2 t) t3) (subst0 i0 v t3 (THead k u2 t)))) (or4_ind
577 (eq T u2 u2) (ex2 T (\lambda (t3: T).(subst0 i0 v u2 t3)) (\lambda (t3:
578 T).(subst0 i0 v u2 t3))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T
579 (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
580 u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v
581 (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)))
582 (\lambda (_: (eq T u2 u2)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x))
583 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
584 T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1
585 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)) (ex_intro2 T (\lambda (t3:
586 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1
587 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5 u2) (subst0_fst v u2 u1 i0
588 H0 x k)))) (\lambda (H6: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda
589 (t: T).(subst0 i0 v u2 t)))).(ex2_ind T (\lambda (t3: T).(subst0 i0 v u2 t3))
590 (\lambda (t3: T).(subst0 i0 v u2 t3)) (or4 (eq T (THead k u2 t) (THead k u1
591 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
592 T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1
593 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t))) (\lambda (x0: T).(\lambda
594 (_: (subst0 i0 v u2 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro1 (eq T
595 (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
596 u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v
597 (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t))
598 (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
599 T).(subst0 i0 v (THead k u1 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5
600 u2) (subst0_fst v u2 u1 i0 H0 x k)))))) H6)) (\lambda (_: (subst0 i0 v u2
601 u2)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3:
602 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1
603 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1
604 x) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t)
605 t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3)) (THead k u2 x)
606 (subst0_snd k v x t i0 H5 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (_:
607 (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T
608 (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0
609 v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0
610 v (THead k u1 x) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v
611 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3)) (THead
612 k u2 x) (subst0_snd k v x t i0 H5 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (H1
613 u2 H0)) t2 H4)))) H3)) (\lambda (H3: (ex3_2 T T (\lambda (u2: T).(\lambda
614 (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0
615 i0 v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i0) v t
616 t2))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead k u3
617 t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_:
618 T).(\lambda (t3: T).(subst0 (s k i0) v t t3))) (or4 (eq T (THead k u2 t) t2)
619 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
620 T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2
621 (THead k u2 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t2
622 (THead k x0 x1))).(\lambda (H5: (subst0 i0 v u1 x0)).(\lambda (H6: (subst0 (s
623 k i0) v t x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(or4 (eq T (THead
624 k u2 t) t3) (ex2 T (\lambda (t4: T).(subst0 i0 v (THead k u2 t) t4)) (\lambda
625 (t4: T).(subst0 i0 v t3 t4))) (subst0 i0 v (THead k u2 t) t3) (subst0 i0 v t3
626 (THead k u2 t)))) (or4_ind (eq T u2 x0) (ex2 T (\lambda (t3: T).(subst0 i0 v
627 u2 t3)) (\lambda (t3: T).(subst0 i0 v x0 t3))) (subst0 i0 v u2 x0) (subst0 i0
628 v x0 u2) (or4 (eq T (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3:
629 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0
630 x1) t3))) (subst0 i0 v (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k
631 x0 x1) (THead k u2 t))) (\lambda (H7: (eq T u2 x0)).(eq_ind_r T x0 (\lambda
632 (t3: T).(or4 (eq T (THead k t3 t) (THead k x0 x1)) (ex2 T (\lambda (t4:
633 T).(subst0 i0 v (THead k t3 t) t4)) (\lambda (t4: T).(subst0 i0 v (THead k x0
634 x1) t4))) (subst0 i0 v (THead k t3 t) (THead k x0 x1)) (subst0 i0 v (THead k
635 x0 x1) (THead k t3 t)))) (or4_intro2 (eq T (THead k x0 t) (THead k x0 x1))
636 (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k x0 t) t3)) (\lambda (t3:
637 T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k x0 t) (THead k x0
638 x1)) (subst0 i0 v (THead k x0 x1) (THead k x0 t)) (subst0_snd k v x1 t i0 H6
639 x0)) u2 H7)) (\lambda (H7: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t))
640 (\lambda (t: T).(subst0 i0 v x0 t)))).(ex2_ind T (\lambda (t3: T).(subst0 i0
641 v u2 t3)) (\lambda (t3: T).(subst0 i0 v x0 t3)) (or4 (eq T (THead k u2 t)
642 (THead k x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
643 (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k u2
644 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t))) (\lambda
645 (x: T).(\lambda (H8: (subst0 i0 v u2 x)).(\lambda (H9: (subst0 i0 v x0
646 x)).(or4_intro1 (eq T (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3:
647 T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0
648 x1) t3))) (subst0 i0 v (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k
649 x0 x1) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2
650 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3)) (THead k x x1)
651 (subst0_both v u2 x i0 H8 k t x1 H6) (subst0_fst v x x0 i0 H9 x1 k)))))) H7))
652 (\lambda (H7: (subst0 i0 v u2 x0)).(or4_intro2 (eq T (THead k u2 t) (THead k
653 x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda
654 (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v (THead k u2 t) (THead
655 k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t)) (subst0_both v u2 x0
656 i0 H7 k t x1 H6))) (\lambda (H7: (subst0 i0 v x0 u2)).(or4_intro1 (eq T
657 (THead k u2 t) (THead k x0 x1)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
658 u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x0 x1) t3))) (subst0 i0 v
659 (THead k u2 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t))
660 (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
661 T).(subst0 i0 v (THead k x0 x1) t3)) (THead k u2 x1) (subst0_snd k v x1 t i0
662 H6 u2) (subst0_fst v u2 x0 i0 H7 x1 k)))) (H1 x0 H5)) t2 H4)))))) H3))
663 (subst0_gen_head k v u1 t t2 i0 H2)))))))))))) (\lambda (k: K).(\lambda (v:
664 T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (H0: (subst0
665 (s k i0) v t3 t2)).(\lambda (H1: ((\forall (t4: T).((subst0 (s k i0) v t3 t4)
666 \to (or4 (eq T t2 t4) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
667 (\lambda (t: T).(subst0 (s k i0) v t4 t))) (subst0 (s k i0) v t2 t4) (subst0
668 (s k i0) v t4 t2)))))).(\lambda (u0: T).(\lambda (t4: T).(\lambda (H2:
669 (subst0 i0 v (THead k u0 t3) t4)).(or3_ind (ex2 T (\lambda (u2: T).(eq T t4
670 (THead k u2 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2))) (ex2 T (\lambda (t5:
671 T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i0) v t3 t5)))
672 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead k u2 t5))))
673 (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_:
674 T).(\lambda (t5: T).(subst0 (s k i0) v t3 t5)))) (or4 (eq T (THead k u0 t2)
675 t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
676 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2) t4) (subst0 i0 v t4
677 (THead k u0 t2))) (\lambda (H3: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2
678 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2)))).(ex2_ind T (\lambda (u2: T).(eq
679 T t4 (THead k u2 t3))) (\lambda (u2: T).(subst0 i0 v u0 u2)) (or4 (eq T
680 (THead k u0 t2) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
681 (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2) t4) (subst0
682 i0 v t4 (THead k u0 t2))) (\lambda (x: T).(\lambda (H4: (eq T t4 (THead k x
683 t3))).(\lambda (H5: (subst0 i0 v u0 x)).(eq_ind_r T (THead k x t3) (\lambda
684 (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T (\lambda (t5: T).(subst0 i0 v
685 (THead k u0 t2) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
686 (THead k u0 t2) t) (subst0 i0 v t (THead k u0 t2)))) (or4_ind (eq T t2 t2)
687 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k
688 i0) v t2 t))) (subst0 (s k i0) v t2 t2) (subst0 (s k i0) v t2 t2) (or4 (eq T
689 (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
690 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v
691 (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)))
692 (\lambda (_: (eq T t2 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3))
693 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
694 T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x
695 t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
696 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
697 t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3
698 i0 H0 x)))) (\lambda (H6: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
699 (\lambda (t: T).(subst0 (s k i0) v t2 t)))).(ex2_ind T (\lambda (t:
700 T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k i0) v t2 t)) (or4
701 (eq T (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v
702 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0
703 i0 v (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0
704 t2))) (\lambda (x0: T).(\lambda (_: (subst0 (s k i0) v t2 x0)).(\lambda (_:
705 (subst0 (s k i0) v t2 x0)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3))
706 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
707 T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x
708 t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
709 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
710 t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3
711 i0 H0 x)))))) H6)) (\lambda (_: (subst0 (s k i0) v t2 t2)).(or4_intro1 (eq T
712 (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
713 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t))) (subst0 i0 v
714 (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x t3) (THead k u0 t2))
715 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
716 T).(subst0 i0 v (THead k x t3) t)) (THead k x t2) (subst0_fst v x u0 i0 H5 t2
717 k) (subst0_snd k v t2 t3 i0 H0 x)))) (\lambda (_: (subst0 (s k i0) v t2
718 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x t3)) (ex2 T (\lambda (t:
719 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x
720 t3) t))) (subst0 i0 v (THead k u0 t2) (THead k x t3)) (subst0 i0 v (THead k x
721 t3) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0
722 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (THead k x t2)
723 (subst0_fst v x u0 i0 H5 t2 k) (subst0_snd k v t2 t3 i0 H0 x)))) (H1 t2 H0))
724 t4 H4)))) H3)) (\lambda (H3: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u0
725 t2))) (\lambda (t2: T).(subst0 (s k i0) v t3 t2)))).(ex2_ind T (\lambda (t5:
726 T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i0) v t3 t5))
727 (or4 (eq T (THead k u0 t2) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
728 u0 t2) t)) (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u0 t2)
729 t4) (subst0 i0 v t4 (THead k u0 t2))) (\lambda (x: T).(\lambda (H4: (eq T t4
730 (THead k u0 x))).(\lambda (H5: (subst0 (s k i0) v t3 x)).(eq_ind_r T (THead k
731 u0 x) (\lambda (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T (\lambda (t5:
732 T).(subst0 i0 v (THead k u0 t2) t5)) (\lambda (t5: T).(subst0 i0 v t t5)))
733 (subst0 i0 v (THead k u0 t2) t) (subst0 i0 v t (THead k u0 t2)))) (or4_ind
734 (eq T t2 x) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t:
735 T).(subst0 (s k i0) v x t))) (subst0 (s k i0) v t2 x) (subst0 (s k i0) v x
736 t2) (or4 (eq T (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0
737 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)))
738 (subst0 i0 v (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0 x)
739 (THead k u0 t2))) (\lambda (H6: (eq T t2 x)).(eq_ind_r T x (\lambda (t:
740 T).(or4 (eq T (THead k u0 t) (THead k u0 x)) (ex2 T (\lambda (t5: T).(subst0
741 i0 v (THead k u0 t) t5)) (\lambda (t5: T).(subst0 i0 v (THead k u0 x) t5)))
742 (subst0 i0 v (THead k u0 t) (THead k u0 x)) (subst0 i0 v (THead k u0 x)
743 (THead k u0 t)))) (or4_intro0 (eq T (THead k u0 x) (THead k u0 x)) (ex2 T
744 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)) (\lambda (t: T).(subst0 i0 v
745 (THead k u0 x) t))) (subst0 i0 v (THead k u0 x) (THead k u0 x)) (subst0 i0 v
746 (THead k u0 x) (THead k u0 x)) (refl_equal T (THead k u0 x))) t2 H6))
747 (\lambda (H6: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t)) (\lambda (t:
748 T).(subst0 (s k i0) v x t)))).(ex2_ind T (\lambda (t: T).(subst0 (s k i0) v
749 t2 t)) (\lambda (t: T).(subst0 (s k i0) v x t)) (or4 (eq T (THead k u0 t2)
750 (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
751 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v (THead k u0 t2)
752 (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2))) (\lambda (x0:
753 T).(\lambda (H7: (subst0 (s k i0) v t2 x0)).(\lambda (H8: (subst0 (s k i0) v
754 x x0)).(or4_intro1 (eq T (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t:
755 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0
756 x) t))) (subst0 i0 v (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0
757 x) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2)
758 t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t)) (THead k u0 x0)
759 (subst0_snd k v x0 t2 i0 H7 u0) (subst0_snd k v x0 x i0 H8 u0)))))) H6))
760 (\lambda (H6: (subst0 (s k i0) v t2 x)).(or4_intro2 (eq T (THead k u0 t2)
761 (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t))
762 (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v (THead k u0 t2)
763 (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2)) (subst0_snd k v
764 x t2 i0 H6 u0))) (\lambda (H6: (subst0 (s k i0) v x t2)).(or4_intro3 (eq T
765 (THead k u0 t2) (THead k u0 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
766 u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k u0 x) t))) (subst0 i0 v
767 (THead k u0 t2) (THead k u0 x)) (subst0 i0 v (THead k u0 x) (THead k u0 t2))
768 (subst0_snd k v t2 x i0 H6 u0))) (H1 x H5)) t4 H4)))) H3)) (\lambda (H3:
769 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2))))
770 (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_:
771 T).(\lambda (t2: T).(subst0 (s k i0) v t3 t2))))).(ex3_2_ind T T (\lambda
772 (u2: T).(\lambda (t5: T).(eq T t4 (THead k u2 t5)))) (\lambda (u2:
773 T).(\lambda (_: T).(subst0 i0 v u0 u2))) (\lambda (_: T).(\lambda (t5:
774 T).(subst0 (s k i0) v t3 t5))) (or4 (eq T (THead k u0 t2) t4) (ex2 T (\lambda
775 (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v t4 t)))
776 (subst0 i0 v (THead k u0 t2) t4) (subst0 i0 v t4 (THead k u0 t2))) (\lambda
777 (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t4 (THead k x0 x1))).(\lambda
778 (H5: (subst0 i0 v u0 x0)).(\lambda (H6: (subst0 (s k i0) v t3 x1)).(eq_ind_r
779 T (THead k x0 x1) (\lambda (t: T).(or4 (eq T (THead k u0 t2) t) (ex2 T
780 (\lambda (t5: T).(subst0 i0 v (THead k u0 t2) t5)) (\lambda (t5: T).(subst0
781 i0 v t t5))) (subst0 i0 v (THead k u0 t2) t) (subst0 i0 v t (THead k u0
782 t2)))) (or4_ind (eq T t2 x1) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
783 (\lambda (t: T).(subst0 (s k i0) v x1 t))) (subst0 (s k i0) v t2 x1) (subst0
784 (s k i0) v x1 t2) (or4 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda
785 (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k
786 x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead
787 k x0 x1) (THead k u0 t2))) (\lambda (H7: (eq T t2 x1)).(eq_ind_r T x1
788 (\lambda (t: T).(or4 (eq T (THead k u0 t) (THead k x0 x1)) (ex2 T (\lambda
789 (t5: T).(subst0 i0 v (THead k u0 t) t5)) (\lambda (t5: T).(subst0 i0 v (THead
790 k x0 x1) t5))) (subst0 i0 v (THead k u0 t) (THead k x0 x1)) (subst0 i0 v
791 (THead k x0 x1) (THead k u0 t)))) (or4_intro2 (eq T (THead k u0 x1) (THead k
792 x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 x1) t)) (\lambda (t:
793 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u0 x1) (THead k x0
794 x1)) (subst0 i0 v (THead k x0 x1) (THead k u0 x1)) (subst0_fst v x0 u0 i0 H5
795 x1 k)) t2 H7)) (\lambda (H7: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t2 t))
796 (\lambda (t: T).(subst0 (s k i0) v x1 t)))).(ex2_ind T (\lambda (t:
797 T).(subst0 (s k i0) v t2 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)) (or4
798 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
799 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
800 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
801 u0 t2))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i0) v t2 x)).(\lambda
802 (H9: (subst0 (s k i0) v x1 x)).(or4_intro1 (eq T (THead k u0 t2) (THead k x0
803 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t:
804 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0
805 x1)) (subst0 i0 v (THead k x0 x1) (THead k u0 t2)) (ex_intro2 T (\lambda (t:
806 T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
807 x1) t)) (THead k x0 x) (subst0_both v u0 x0 i0 H5 k t2 x H8) (subst0_snd k v
808 x x1 i0 H9 x0)))))) H7)) (\lambda (H7: (subst0 (s k i0) v t2 x1)).(or4_intro2
809 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
810 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
811 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
812 u0 t2)) (subst0_both v u0 x0 i0 H5 k t2 x1 H7))) (\lambda (H7: (subst0 (s k
813 i0) v x1 t2)).(or4_intro1 (eq T (THead k u0 t2) (THead k x0 x1)) (ex2 T
814 (\lambda (t: T).(subst0 i0 v (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v
815 (THead k x0 x1) t))) (subst0 i0 v (THead k u0 t2) (THead k x0 x1)) (subst0 i0
816 v (THead k x0 x1) (THead k u0 t2)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
817 (THead k u0 t2) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k
818 x0 t2) (subst0_fst v x0 u0 i0 H5 t2 k) (subst0_snd k v t2 x1 i0 H7 x0)))) (H1
819 x1 H6)) t4 H4)))))) H3)) (subst0_gen_head k v u0 t3 t4 i0 H2))))))))))))
820 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda
821 (H0: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (t2: T).((subst0 i0 v u1
822 t2) \to (or4 (eq T u2 t2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda
823 (t: T).(subst0 i0 v t2 t))) (subst0 i0 v u2 t2) (subst0 i0 v t2
824 u2)))))).(\lambda (k: K).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2:
825 (subst0 (s k i0) v t2 t3)).(\lambda (H3: ((\forall (t4: T).((subst0 (s k i0)
826 v t2 t4) \to (or4 (eq T t3 t4) (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3
827 t)) (\lambda (t: T).(subst0 (s k i0) v t4 t))) (subst0 (s k i0) v t3 t4)
828 (subst0 (s k i0) v t4 t3)))))).(\lambda (t4: T).(\lambda (H4: (subst0 i0 v
829 (THead k u1 t2) t4)).(or3_ind (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3
830 t2))) (\lambda (u3: T).(subst0 i0 v u1 u3))) (ex2 T (\lambda (t5: T).(eq T t4
831 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i0) v t2 t5))) (ex3_2 T T
832 (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3:
833 T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_: T).(\lambda (t5:
834 T).(subst0 (s k i0) v t2 t5)))) (or4 (eq T (THead k u2 t3) t4) (ex2 T
835 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
836 t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4 (THead k u2 t3)))
837 (\lambda (H5: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2 t2))) (\lambda
838 (u2: T).(subst0 i0 v u1 u2)))).(ex2_ind T (\lambda (u3: T).(eq T t4 (THead k
839 u3 t2))) (\lambda (u3: T).(subst0 i0 v u1 u3)) (or4 (eq T (THead k u2 t3) t4)
840 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
841 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4
842 (THead k u2 t3))) (\lambda (x: T).(\lambda (H6: (eq T t4 (THead k x
843 t2))).(\lambda (H7: (subst0 i0 v u1 x)).(eq_ind_r T (THead k x t2) (\lambda
844 (t: T).(or4 (eq T (THead k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0 i0 v
845 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
846 (THead k u2 t3) t) (subst0 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 t3)
847 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k
848 i0) v t3 t))) (subst0 (s k i0) v t3 t3) (subst0 (s k i0) v t3 t3) (or4 (eq T
849 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
850 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
851 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)))
852 (\lambda (_: (eq T t3 t3)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t:
853 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x)
854 (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
855 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
856 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
857 x t2) (THead k u2 t3))) (\lambda (H9: (eq T u2 x)).(eq_ind_r T x (\lambda (t:
858 T).(or4 (eq T (THead k t t3) (THead k x t2)) (ex2 T (\lambda (t5: T).(subst0
859 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x t2) t5)))
860 (subst0 i0 v (THead k t t3) (THead k x t2)) (subst0 i0 v (THead k x t2)
861 (THead k t t3)))) (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T
862 (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v
863 (THead k x t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v
864 (THead k x t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H9))
865 (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
866 T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
867 (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2))
868 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
869 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
870 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x0: T).(\lambda
871 (H10: (subst0 i0 v u2 x0)).(\lambda (H11: (subst0 i0 v x x0)).(or4_intro1 (eq
872 T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
873 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
874 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
875 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
876 T).(subst0 i0 v (THead k x t2) t)) (THead k x0 t3) (subst0_fst v x0 u2 i0 H10
877 t3 k) (subst0_both v x x0 i0 H11 k t2 t3 H2)))))) H9)) (\lambda (H9: (subst0
878 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
879 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
880 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
881 x t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
882 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x t3)
883 (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd k v t3 t2 i0 H2 x)))) (\lambda
884 (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k x t2))
885 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
886 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
887 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H9 k
888 t2 t3 H2))) (H1 x H7))) (\lambda (H8: (ex2 T (\lambda (t: T).(subst0 (s k i0)
889 v t3 t)) (\lambda (t: T).(subst0 (s k i0) v t3 t)))).(ex2_ind T (\lambda (t:
890 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v t3 t)) (or4
891 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v
892 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0
893 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2
894 t3))) (\lambda (x0: T).(\lambda (_: (subst0 (s k i0) v t3 x0)).(\lambda (_:
895 (subst0 (s k i0) v t3 x0)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t:
896 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x)
897 (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda
898 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
899 x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k
900 x t2) (THead k u2 t3))) (\lambda (H11: (eq T u2 x)).(eq_ind_r T x (\lambda
901 (t: T).(or4 (eq T (THead k t t3) (THead k x t2)) (ex2 T (\lambda (t5:
902 T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x
903 t2) t5))) (subst0 i0 v (THead k t t3) (THead k x t2)) (subst0 i0 v (THead k x
904 t2) (THead k t t3)))) (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T
905 (\lambda (t: T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v
906 (THead k x t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v
907 (THead k x t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H11))
908 (\lambda (H11: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
909 T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
910 (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2))
911 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
912 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
913 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x1: T).(\lambda
914 (H12: (subst0 i0 v u2 x1)).(\lambda (H13: (subst0 i0 v x x1)).(or4_intro1 (eq
915 T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
916 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
917 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
918 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
919 T).(subst0 i0 v (THead k x t2) t)) (THead k x1 t3) (subst0_fst v x1 u2 i0 H12
920 t3 k) (subst0_both v x x1 i0 H13 k t2 t3 H2)))))) H11)) (\lambda (H11:
921 (subst0 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T
922 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
923 (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v
924 (THead k x t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
925 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k
926 x t3) (subst0_fst v x u2 i0 H11 t3 k) (subst0_snd k v t3 t2 i0 H2 x))))
927 (\lambda (H11: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k
928 x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
929 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
930 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H11
931 k t2 t3 H2))) (H1 x H7))))) H8)) (\lambda (_: (subst0 (s k i0) v t3
932 t3)).(or4_ind (eq T u2 x) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda
933 (t: T).(subst0 i0 v x t))) (subst0 i0 v u2 x) (subst0 i0 v x u2) (or4 (eq T
934 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
935 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
936 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)))
937 (\lambda (H9: (eq T u2 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k
938 t t3) (THead k x t2)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3)
939 t5)) (\lambda (t5: T).(subst0 i0 v (THead k x t2) t5))) (subst0 i0 v (THead k
940 t t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k t t3))))
941 (or4_intro3 (eq T (THead k x t3) (THead k x t2)) (ex2 T (\lambda (t:
942 T).(subst0 i0 v (THead k x t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
943 t2) t))) (subst0 i0 v (THead k x t3) (THead k x t2)) (subst0 i0 v (THead k x
944 t2) (THead k x t3)) (subst0_snd k v t3 t2 i0 H2 x)) u2 H9)) (\lambda (H9:
945 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x
946 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0
947 i0 v x t)) (or4 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
948 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
949 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
950 t2) (THead k u2 t3))) (\lambda (x0: T).(\lambda (H10: (subst0 i0 v u2
951 x0)).(\lambda (H11: (subst0 i0 v x x0)).(or4_intro1 (eq T (THead k u2 t3)
952 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
953 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
954 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (ex_intro2 T
955 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
956 (THead k x t2) t)) (THead k x0 t3) (subst0_fst v x0 u2 i0 H10 t3 k)
957 (subst0_both v x x0 i0 H11 k t2 t3 H2)))))) H9)) (\lambda (H9: (subst0 i0 v
958 u2 x)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
959 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
960 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
961 t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
962 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x t3)
963 (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd k v t3 t2 i0 H2 x)))) (\lambda
964 (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k x t2))
965 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
966 T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x
967 t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (subst0_both v x u2 i0 H9 k
968 t2 t3 H2))) (H1 x H7))) (\lambda (_: (subst0 (s k i0) v t3 t3)).(or4_ind (eq
969 T u2 x) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0
970 v x t))) (subst0 i0 v u2 x) (subst0 i0 v x u2) (or4 (eq T (THead k u2 t3)
971 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
972 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
973 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (H9:
974 (eq T u2 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k t t3) (THead k
975 x t2)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5:
976 T).(subst0 i0 v (THead k x t2) t5))) (subst0 i0 v (THead k t t3) (THead k x
977 t2)) (subst0 i0 v (THead k x t2) (THead k t t3)))) (or4_intro3 (eq T (THead k
978 x t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k x t3) t))
979 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k x t3)
980 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k x t3)) (subst0_snd k v
981 t3 t2 i0 H2 x)) u2 H9)) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2
982 t)) (\lambda (t: T).(subst0 i0 v x t)))).(ex2_ind T (\lambda (t: T).(subst0
983 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x t)) (or4 (eq T (THead k u2 t3)
984 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
985 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
986 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))) (\lambda (x0:
987 T).(\lambda (H10: (subst0 i0 v u2 x0)).(\lambda (H11: (subst0 i0 v x
988 x0)).(or4_intro1 (eq T (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t:
989 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x
990 t2) t))) (subst0 i0 v (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x
991 t2) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
992 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t)) (THead k x0 t3)
993 (subst0_fst v x0 u2 i0 H10 t3 k) (subst0_both v x x0 i0 H11 k t2 t3 H2))))))
994 H9)) (\lambda (H9: (subst0 i0 v u2 x)).(or4_intro1 (eq T (THead k u2 t3)
995 (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
996 (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v (THead k u2 t3)
997 (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3)) (ex_intro2 T
998 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
999 (THead k x t2) t)) (THead k x t3) (subst0_fst v x u2 i0 H9 t3 k) (subst0_snd
1000 k v t3 t2 i0 H2 x)))) (\lambda (H9: (subst0 i0 v x u2)).(or4_intro3 (eq T
1001 (THead k u2 t3) (THead k x t2)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1002 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x t2) t))) (subst0 i0 v
1003 (THead k u2 t3) (THead k x t2)) (subst0 i0 v (THead k x t2) (THead k u2 t3))
1004 (subst0_both v x u2 i0 H9 k t2 t3 H2))) (H1 x H7))) (H3 t3 H2)) t4 H6))))
1005 H5)) (\lambda (H5: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u1 t2)))
1006 (\lambda (t3: T).(subst0 (s k i0) v t2 t3)))).(ex2_ind T (\lambda (t5: T).(eq
1007 T t4 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i0) v t2 t5)) (or4 (eq T
1008 (THead k u2 t3) t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1009 (\lambda (t: T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0
1010 i0 v t4 (THead k u2 t3))) (\lambda (x: T).(\lambda (H6: (eq T t4 (THead k u1
1011 x))).(\lambda (H7: (subst0 (s k i0) v t2 x)).(eq_ind_r T (THead k u1 x)
1012 (\lambda (t: T).(or4 (eq T (THead k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0
1013 i0 v (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v
1014 (THead k u2 t3) t) (subst0 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 x)
1015 (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k
1016 i0) v x t))) (subst0 (s k i0) v t3 x) (subst0 (s k i0) v x t3) (or4 (eq T
1017 (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1018 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1019 (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)))
1020 (\lambda (H8: (eq T t3 x)).(eq_ind_r T x (\lambda (t: T).(or4 (eq T (THead k
1021 u2 t) (THead k u1 x)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t)
1022 t5)) (\lambda (t5: T).(subst0 i0 v (THead k u1 x) t5))) (subst0 i0 v (THead k
1023 u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)))) (or4_ind
1024 (eq T u2 u2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1025 T).(subst0 i0 v u2 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T
1026 (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1027 u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1028 (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x)))
1029 (\lambda (_: (eq T u2 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x))
1030 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t:
1031 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1
1032 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x
1033 k))) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1034 T).(subst0 i0 v u2 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1035 (\lambda (t: T).(subst0 i0 v u2 t)) (or4 (eq T (THead k u2 x) (THead k u1 x))
1036 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t:
1037 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1
1038 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x))) (\lambda (x0: T).(\lambda
1039 (_: (subst0 i0 v u2 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro3 (eq T
1040 (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1041 u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1042 (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 x))
1043 (subst0_fst v u2 u1 i0 H0 x k))))) H9)) (\lambda (_: (subst0 i0 v u2
1044 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t:
1045 T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1046 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1
1047 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x k))) (\lambda (_: (subst0 i0 v
1048 u2 u2)).(or4_intro3 (eq T (THead k u2 x) (THead k u1 x)) (ex2 T (\lambda (t:
1049 T).(subst0 i0 v (THead k u2 x) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1050 x) t))) (subst0 i0 v (THead k u2 x) (THead k u1 x)) (subst0 i0 v (THead k u1
1051 x) (THead k u2 x)) (subst0_fst v u2 u1 i0 H0 x k))) (H1 u2 H0)) t3 H8))
1052 (\lambda (H8: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3 t)) (\lambda (t:
1053 T).(subst0 (s k i0) v x t)))).(ex2_ind T (\lambda (t: T).(subst0 (s k i0) v
1054 t3 t)) (\lambda (t: T).(subst0 (s k i0) v x t)) (or4 (eq T (THead k u2 t3)
1055 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1056 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1057 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (x0:
1058 T).(\lambda (H9: (subst0 (s k i0) v t3 x0)).(\lambda (H10: (subst0 (s k i0) v
1059 x x0)).(or4_ind (eq T u2 u2) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t))
1060 (\lambda (t: T).(subst0 i0 v u2 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2)
1061 (or4 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0
1062 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)))
1063 (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x)
1064 (THead k u2 t3))) (\lambda (_: (eq T u2 u2)).(or4_intro1 (eq T (THead k u2
1065 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1066 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1067 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (ex_intro2 T
1068 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1069 (THead k u1 x) t)) (THead k u2 x0) (subst0_snd k v x0 t3 i0 H9 u2)
1070 (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (\lambda (H11: (ex2 T (\lambda (t:
1071 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)))).(ex2_ind T
1072 (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)) (or4
1073 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v
1074 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0
1075 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2
1076 t3))) (\lambda (x1: T).(\lambda (_: (subst0 i0 v u2 x1)).(\lambda (_: (subst0
1077 i0 v u2 x1)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1078 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1079 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1080 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1081 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1082 u2 x0) (subst0_snd k v x0 t3 i0 H9 u2) (subst0_both v u1 u2 i0 H0 k x x0
1083 H10)))))) H11)) (\lambda (_: (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead k
1084 u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1085 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2
1086 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (ex_intro2 T
1087 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1088 (THead k u1 x) t)) (THead k u2 x0) (subst0_snd k v x0 t3 i0 H9 u2)
1089 (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (\lambda (_: (subst0 i0 v u2
1090 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1091 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1092 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1093 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1094 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x0)
1095 (subst0_snd k v x0 t3 i0 H9 u2) (subst0_both v u1 u2 i0 H0 k x x0 H10)))) (H1
1096 u2 H0))))) H8)) (\lambda (H8: (subst0 (s k i0) v t3 x)).(or4_ind (eq T u2 u2)
1097 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2
1098 t))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t3)
1099 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1100 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1101 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (_:
1102 (eq T u2 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1103 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1104 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1105 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1106 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1107 u2 x) (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k))))
1108 (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1109 T).(subst0 i0 v u2 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1110 (\lambda (t: T).(subst0 i0 v u2 t)) (or4 (eq T (THead k u2 t3) (THead k u1
1111 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1112 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1
1113 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (x0: T).(\lambda
1114 (_: (subst0 i0 v u2 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro1 (eq T
1115 (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1116 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v
1117 (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))
1118 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1119 T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x) (subst0_snd k v x t3 i0 H8
1120 u2) (subst0_fst v u2 u1 i0 H0 x k)))))) H9)) (\lambda (_: (subst0 i0 v u2
1121 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1122 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1123 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1124 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1125 t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k u2 x)
1126 (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (_:
1127 (subst0 i0 v u2 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T
1128 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1129 (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v
1130 (THead k u1 x) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v
1131 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t)) (THead k
1132 u2 x) (subst0_snd k v x t3 i0 H8 u2) (subst0_fst v u2 u1 i0 H0 x k)))) (H1 u2
1133 H0))) (\lambda (H8: (subst0 (s k i0) v x t3)).(or4_ind (eq T u2 u2) (ex2 T
1134 (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2 t)))
1135 (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t3) (THead k
1136 u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1137 T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1
1138 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3))) (\lambda (_: (eq T u2
1139 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1140 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1141 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1142 x) (THead k u2 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (\lambda (H9:
1143 (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v u2
1144 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0
1145 i0 v u2 t)) (or4 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1146 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1147 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1148 x) (THead k u2 t3))) (\lambda (x0: T).(\lambda (_: (subst0 i0 v u2
1149 x0)).(\lambda (_: (subst0 i0 v u2 x0)).(or4_intro3 (eq T (THead k u2 t3)
1150 (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1151 (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0 i0 v (THead k u2 t3)
1152 (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t3)) (subst0_both v
1153 u1 u2 i0 H0 k x t3 H8))))) H9)) (\lambda (_: (subst0 i0 v u2 u2)).(or4_intro3
1154 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t: T).(subst0 i0 v
1155 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1 x) t))) (subst0
1156 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2
1157 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (\lambda (_: (subst0 i0 v u2
1158 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead k u1 x)) (ex2 T (\lambda (t:
1159 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k u1
1160 x) t))) (subst0 i0 v (THead k u2 t3) (THead k u1 x)) (subst0 i0 v (THead k u1
1161 x) (THead k u2 t3)) (subst0_both v u1 u2 i0 H0 k x t3 H8))) (H1 u2 H0))) (H3
1162 x H7)) t4 H6)))) H5)) (\lambda (H5: (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1163 T).(eq T t4 (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i0 v
1164 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i0) v t2
1165 t3))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3
1166 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i0 v u1 u3))) (\lambda (_:
1167 T).(\lambda (t5: T).(subst0 (s k i0) v t2 t5))) (or4 (eq T (THead k u2 t3)
1168 t4) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1169 T).(subst0 i0 v t4 t))) (subst0 i0 v (THead k u2 t3) t4) (subst0 i0 v t4
1170 (THead k u2 t3))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H6: (eq T t4
1171 (THead k x0 x1))).(\lambda (H7: (subst0 i0 v u1 x0)).(\lambda (H8: (subst0 (s
1172 k i0) v t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(or4 (eq T (THead
1173 k u2 t3) t) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t3) t5))
1174 (\lambda (t5: T).(subst0 i0 v t t5))) (subst0 i0 v (THead k u2 t3) t) (subst0
1175 i0 v t (THead k u2 t3)))) (or4_ind (eq T t3 x1) (ex2 T (\lambda (t:
1176 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)))
1177 (subst0 (s k i0) v t3 x1) (subst0 (s k i0) v x1 t3) (or4 (eq T (THead k u2
1178 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1179 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1180 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1181 (H9: (eq T t3 x1)).(eq_ind_r T x1 (\lambda (t: T).(or4 (eq T (THead k u2 t)
1182 (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k u2 t) t5))
1183 (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v (THead k u2
1184 t) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t)))) (or4_ind
1185 (eq T u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1186 T).(subst0 i0 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2) (or4 (eq T
1187 (THead k u2 x1) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k
1188 u2 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v
1189 (THead k u2 x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2
1190 x1))) (\lambda (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t: T).(or4 (eq T
1191 (THead k t x1) (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k
1192 t x1) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v
1193 (THead k t x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k t
1194 x1)))) (or4_intro0 (eq T (THead k x0 x1) (THead k x0 x1)) (ex2 T (\lambda (t:
1195 T).(subst0 i0 v (THead k x0 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1196 x1) t))) (subst0 i0 v (THead k x0 x1) (THead k x0 x1)) (subst0 i0 v (THead k
1197 x0 x1) (THead k x0 x1)) (refl_equal T (THead k x0 x1))) u2 H10)) (\lambda
1198 (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v
1199 x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1200 T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2 T
1201 (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0 v
1202 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0 i0
1203 v (THead k x0 x1) (THead k u2 x1))) (\lambda (x: T).(\lambda (H11: (subst0 i0
1204 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq T (THead k u2 x1)
1205 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t))
1206 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1207 x1) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 x1)) (ex_intro2
1208 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0
1209 v (THead k x0 x1) t)) (THead k x x1) (subst0_fst v x u2 i0 H11 x1 k)
1210 (subst0_fst v x x0 i0 H12 x1 k)))))) H10)) (\lambda (H10: (subst0 i0 v u2
1211 x0)).(or4_intro2 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2 T (\lambda (t:
1212 T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1213 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0 i0 v (THead k
1214 x0 x1) (THead k u2 x1)) (subst0_fst v x0 u2 i0 H10 x1 k))) (\lambda (H10:
1215 (subst0 i0 v x0 u2)).(or4_intro3 (eq T (THead k u2 x1) (THead k x0 x1)) (ex2
1216 T (\lambda (t: T).(subst0 i0 v (THead k u2 x1) t)) (\lambda (t: T).(subst0 i0
1217 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 x1) (THead k x0 x1)) (subst0
1218 i0 v (THead k x0 x1) (THead k u2 x1)) (subst0_fst v u2 x0 i0 H10 x1 k))) (H1
1219 x0 H7)) t3 H9)) (\lambda (H9: (ex2 T (\lambda (t: T).(subst0 (s k i0) v t3
1220 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)))).(ex2_ind T (\lambda (t:
1221 T).(subst0 (s k i0) v t3 t)) (\lambda (t: T).(subst0 (s k i0) v x1 t)) (or4
1222 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v
1223 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0
1224 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k
1225 u2 t3))) (\lambda (x: T).(\lambda (H10: (subst0 (s k i0) v t3 x)).(\lambda
1226 (H11: (subst0 (s k i0) v x1 x)).(or4_ind (eq T u2 x0) (ex2 T (\lambda (t:
1227 T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x0 t))) (subst0 i0 v u2
1228 x0) (subst0 i0 v x0 u2) (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T
1229 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1230 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0
1231 v (THead k x0 x1) (THead k u2 t3))) (\lambda (H12: (eq T u2 x0)).(eq_ind_r T
1232 x0 (\lambda (t: T).(or4 (eq T (THead k t t3) (THead k x0 x1)) (ex2 T (\lambda
1233 (t5: T).(subst0 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead
1234 k x0 x1) t5))) (subst0 i0 v (THead k t t3) (THead k x0 x1)) (subst0 i0 v
1235 (THead k x0 x1) (THead k t t3)))) (or4_intro1 (eq T (THead k x0 t3) (THead k
1236 x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t:
1237 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0
1238 x1)) (subst0 i0 v (THead k x0 x1) (THead k x0 t3)) (ex_intro2 T (\lambda (t:
1239 T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1240 x1) t)) (THead k x0 x) (subst0_snd k v x t3 i0 H10 x0) (subst0_snd k v x x1
1241 i0 H11 x0))) u2 H12)) (\lambda (H12: (ex2 T (\lambda (t: T).(subst0 i0 v u2
1242 t)) (\lambda (t: T).(subst0 i0 v x0 t)))).(ex2_ind T (\lambda (t: T).(subst0
1243 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3)
1244 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1245 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1246 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1247 (x2: T).(\lambda (H13: (subst0 i0 v u2 x2)).(\lambda (H14: (subst0 i0 v x0
1248 x2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1249 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1250 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1251 x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2
1252 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k x2 x)
1253 (subst0_both v u2 x2 i0 H13 k t3 x H10) (subst0_both v x0 x2 i0 H14 k x1 x
1254 H11)))))) H12)) (\lambda (H12: (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead
1255 k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3)
1256 t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k
1257 u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))
1258 (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1259 T).(subst0 i0 v (THead k x0 x1) t)) (THead k x0 x) (subst0_both v u2 x0 i0
1260 H12 k t3 x H10) (subst0_snd k v x x1 i0 H11 x0)))) (\lambda (H12: (subst0 i0
1261 v x0 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda
1262 (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k
1263 x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead
1264 k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k
1265 u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k u2 x)
1266 (subst0_snd k v x t3 i0 H10 u2) (subst0_both v x0 u2 i0 H12 k x1 x H11))))
1267 (H1 x0 H7))))) H9)) (\lambda (H9: (subst0 (s k i0) v t3 x1)).(or4_ind (eq T
1268 u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0
1269 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2) (or4 (eq T (THead k u2 t3)
1270 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1271 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1272 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda
1273 (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t: T).(or4 (eq T (THead k t t3)
1274 (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0 i0 v (THead k t t3) t5))
1275 (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5))) (subst0 i0 v (THead k t
1276 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k t t3))))
1277 (or4_intro2 (eq T (THead k x0 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1278 T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1279 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1280 x0 x1) (THead k x0 t3)) (subst0_snd k v x1 t3 i0 H9 x0)) u2 H10)) (\lambda
1281 (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t: T).(subst0 i0 v
1282 x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1283 T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T
1284 (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v
1285 (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0
1286 v (THead k x0 x1) (THead k u2 t3))) (\lambda (x: T).(\lambda (H11: (subst0 i0
1287 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq T (THead k u2 t3)
1288 (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t))
1289 (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2
1290 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2
1291 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0
1292 v (THead k x0 x1) t)) (THead k x x1) (subst0_both v u2 x i0 H11 k t3 x1 H9)
1293 (subst0_fst v x x0 i0 H12 x1 k)))))) H10)) (\lambda (H10: (subst0 i0 v u2
1294 x0)).(or4_intro2 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t:
1295 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1296 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k
1297 x0 x1) (THead k u2 t3)) (subst0_both v u2 x0 i0 H10 k t3 x1 H9))) (\lambda
1298 (H10: (subst0 i0 v x0 u2)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1))
1299 (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1300 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0
1301 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t:
1302 T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0
1303 x1) t)) (THead k u2 x1) (subst0_snd k v x1 t3 i0 H9 u2) (subst0_fst v u2 x0
1304 i0 H10 x1 k)))) (H1 x0 H7))) (\lambda (H9: (subst0 (s k i0) v x1
1305 t3)).(or4_ind (eq T u2 x0) (ex2 T (\lambda (t: T).(subst0 i0 v u2 t))
1306 (\lambda (t: T).(subst0 i0 v x0 t))) (subst0 i0 v u2 x0) (subst0 i0 v x0 u2)
1307 (or4 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0
1308 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)))
1309 (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1)
1310 (THead k u2 t3))) (\lambda (H10: (eq T u2 x0)).(eq_ind_r T x0 (\lambda (t:
1311 T).(or4 (eq T (THead k t t3) (THead k x0 x1)) (ex2 T (\lambda (t5: T).(subst0
1312 i0 v (THead k t t3) t5)) (\lambda (t5: T).(subst0 i0 v (THead k x0 x1) t5)))
1313 (subst0 i0 v (THead k t t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1)
1314 (THead k t t3)))) (or4_intro3 (eq T (THead k x0 t3) (THead k x0 x1)) (ex2 T
1315 (\lambda (t: T).(subst0 i0 v (THead k x0 t3) t)) (\lambda (t: T).(subst0 i0 v
1316 (THead k x0 x1) t))) (subst0 i0 v (THead k x0 t3) (THead k x0 x1)) (subst0 i0
1317 v (THead k x0 x1) (THead k x0 t3)) (subst0_snd k v t3 x1 i0 H9 x0)) u2 H10))
1318 (\lambda (H10: (ex2 T (\lambda (t: T).(subst0 i0 v u2 t)) (\lambda (t:
1319 T).(subst0 i0 v x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i0 v u2 t))
1320 (\lambda (t: T).(subst0 i0 v x0 t)) (or4 (eq T (THead k u2 t3) (THead k x0
1321 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t:
1322 T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0
1323 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3))) (\lambda (x: T).(\lambda
1324 (H11: (subst0 i0 v u2 x)).(\lambda (H12: (subst0 i0 v x0 x)).(or4_intro1 (eq
1325 T (THead k u2 t3) (THead k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead
1326 k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v
1327 (THead k u2 t3) (THead k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2
1328 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda
1329 (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead k x t3) (subst0_fst v x u2 i0
1330 H11 t3 k) (subst0_both v x0 x i0 H12 k x1 t3 H9)))))) H10)) (\lambda (H10:
1331 (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead k u2 t3) (THead k x0 x1)) (ex2
1332 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0
1333 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead k x0 x1)) (subst0
1334 i0 v (THead k x0 x1) (THead k u2 t3)) (ex_intro2 T (\lambda (t: T).(subst0 i0
1335 v (THead k u2 t3) t)) (\lambda (t: T).(subst0 i0 v (THead k x0 x1) t)) (THead
1336 k x0 t3) (subst0_fst v x0 u2 i0 H10 t3 k) (subst0_snd k v t3 x1 i0 H9 x0))))
1337 (\lambda (H10: (subst0 i0 v x0 u2)).(or4_intro3 (eq T (THead k u2 t3) (THead
1338 k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda
1339 (t: T).(subst0 i0 v (THead k x0 x1) t))) (subst0 i0 v (THead k u2 t3) (THead
1340 k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (subst0_both v x0 u2
1341 i0 H10 k x1 t3 H9))) (H1 x0 H7))) (H3 x1 H8)) t4 H6)))))) H5))
1342 (subst0_gen_head k v u1 t2 t4 i0 H4))))))))))))))) i u t0 t1 H))))).
1344 theorem subst0_confluence_lift:
1345 \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0
1346 i u t0 (lift (S O) i t1)) \to (\forall (t2: T).((subst0 i u t0 (lift (S O) i
1347 t2)) \to (eq T t1 t2)))))))
1349 \lambda (t0: T).(\lambda (t1: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
1350 (H: (subst0 i u t0 (lift (S O) i t1))).(\lambda (t2: T).(\lambda (H0: (subst0
1351 i u t0 (lift (S O) i t2))).(or4_ind (eq T (lift (S O) i t2) (lift (S O) i
1352 t1)) (ex2 T (\lambda (t: T).(subst0 i u (lift (S O) i t2) t)) (\lambda (t:
1353 T).(subst0 i u (lift (S O) i t1) t))) (subst0 i u (lift (S O) i t2) (lift (S
1354 O) i t1)) (subst0 i u (lift (S O) i t1) (lift (S O) i t2)) (eq T t1 t2)
1355 (\lambda (H1: (eq T (lift (S O) i t2) (lift (S O) i t1))).(let H2 \def
1356 (sym_equal T (lift (S O) i t2) (lift (S O) i t1) H1) in (lift_inj t1 t2 (S O)
1357 i H2))) (\lambda (H1: (ex2 T (\lambda (t: T).(subst0 i u (lift (S O) i t2)
1358 t)) (\lambda (t: T).(subst0 i u (lift (S O) i t1) t)))).(ex2_ind T (\lambda
1359 (t: T).(subst0 i u (lift (S O) i t2) t)) (\lambda (t: T).(subst0 i u (lift (S
1360 O) i t1) t)) (eq T t1 t2) (\lambda (x: T).(\lambda (_: (subst0 i u (lift (S
1361 O) i t2) x)).(\lambda (H3: (subst0 i u (lift (S O) i t1)
1362 x)).(subst0_gen_lift_false t1 u x (S O) i i (le_n i) (eq_ind_r nat (plus (S
1363 O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O))
1364 (plus_comm i (S O))) H3 (eq T t1 t2))))) H1)) (\lambda (H1: (subst0 i u (lift
1365 (S O) i t2) (lift (S O) i t1))).(subst0_gen_lift_false t2 u (lift (S O) i t1)
1366 (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n))
1367 (le_n (plus (S O) i)) (plus i (S O)) (plus_comm i (S O))) H1 (eq T t1 t2)))
1368 (\lambda (H1: (subst0 i u (lift (S O) i t1) (lift (S O) i
1369 t2))).(subst0_gen_lift_false t1 u (lift (S O) i t2) (S O) i i (le_n i)
1370 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O)
1371 i)) (plus i (S O)) (plus_comm i (S O))) H1 (eq T t1 t2)))
1372 (subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).
projects / helm.git / blob