1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0".
19 include "pc3/left.ma".
21 include "fsubst0/defs.ma".
23 include "csubst0/getl.ma".
25 theorem pc3_pr2_fsubst0:
26 \forall (c1: C).(\forall (t1: T).(\forall (t: T).((pr2 c1 t1 t) \to (\forall
27 (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
28 t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
31 \lambda (c1: C).(\lambda (t1: T).(\lambda (t: T).(\lambda (H: (pr2 c1 t1
32 t)).(pr2_ind (\lambda (c: C).(\lambda (t0: T).(\lambda (t2: T).(\forall (i:
33 nat).(\forall (u: T).(\forall (c2: C).(\forall (t3: T).((fsubst0 i u c t0 c2
34 t3) \to (\forall (e: C).((getl i c (CHead e (Bind Abbr) u)) \to (pc3 c2 t3
35 t2))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H0:
36 (pr0 t2 t3)).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t0:
37 T).(\lambda (H1: (fsubst0 i u c t2 c2 t0)).(fsubst0_ind i u c t2 (\lambda
38 (c0: C).(\lambda (t4: T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u))
39 \to (pc3 c0 t4 t3))))) (\lambda (t4: T).(\lambda (H2: (subst0 i u t2
40 t4)).(\lambda (e: C).(\lambda (H3: (getl i c (CHead e (Bind Abbr)
41 u))).(or_ind (pr0 t4 t3) (ex2 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2:
42 T).(subst0 i u t3 w2))) (pc3 c t4 t3) (\lambda (H4: (pr0 t4 t3)).(pc3_pr2_r c
43 t4 t3 (pr2_free c t4 t3 H4))) (\lambda (H4: (ex2 T (\lambda (w2: T).(pr0 t4
44 w2)) (\lambda (w2: T).(subst0 i u t3 w2)))).(ex2_ind T (\lambda (w2: T).(pr0
45 t4 w2)) (\lambda (w2: T).(subst0 i u t3 w2)) (pc3 c t4 t3) (\lambda (x:
46 T).(\lambda (H5: (pr0 t4 x)).(\lambda (H6: (subst0 i u t3 x)).(pc3_pr2_u c x
47 t4 (pr2_free c t4 x H5) t3 (pc3_pr2_x c x t3 (pr2_delta c e u i H3 t3 t3
48 (pr0_refl t3) x H6)))))) H4)) (pr0_subst0 t2 t3 H0 u t4 i H2 u (pr0_refl
49 u))))))) (\lambda (c0: C).(\lambda (_: (csubst0 i u c c0)).(\lambda (e:
50 C).(\lambda (_: (getl i c (CHead e (Bind Abbr) u))).(pc3_pr2_r c0 t2 t3
51 (pr2_free c0 t2 t3 H0)))))) (\lambda (t4: T).(\lambda (H2: (subst0 i u t2
52 t4)).(\lambda (c0: C).(\lambda (H3: (csubst0 i u c c0)).(\lambda (e:
53 C).(\lambda (H4: (getl i c (CHead e (Bind Abbr) u))).(or_ind (pr0 t4 t3) (ex2
54 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2: T).(subst0 i u t3 w2))) (pc3 c0
55 t4 t3) (\lambda (H5: (pr0 t4 t3)).(pc3_pr2_r c0 t4 t3 (pr2_free c0 t4 t3
56 H5))) (\lambda (H5: (ex2 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2:
57 T).(subst0 i u t3 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t4 w2)) (\lambda
58 (w2: T).(subst0 i u t3 w2)) (pc3 c0 t4 t3) (\lambda (x: T).(\lambda (H6: (pr0
59 t4 x)).(\lambda (H7: (subst0 i u t3 x)).(pc3_pr2_u c0 x t4 (pr2_free c0 t4 x
60 H6) t3 (pc3_pr2_x c0 x t3 (pr2_delta c0 e u i (csubst0_getl_ge i i (le_n i) c
61 c0 u H3 (CHead e (Bind Abbr) u) H4) t3 t3 (pr0_refl t3) x H7)))))) H5))
62 (pr0_subst0 t2 t3 H0 u t4 i H2 u (pr0_refl u))))))))) c2 t0 H1))))))))))
63 (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
64 (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t2: T).(\lambda (t3:
65 T).(\lambda (H1: (pr0 t2 t3)).(\lambda (t0: T).(\lambda (H2: (subst0 i u t3
66 t0)).(\lambda (i0: nat).(\lambda (u0: T).(\lambda (c2: C).(\lambda (t4:
67 T).(\lambda (H3: (fsubst0 i0 u0 c t2 c2 t4)).(fsubst0_ind i0 u0 c t2 (\lambda
68 (c0: C).(\lambda (t5: T).(\forall (e: C).((getl i0 c (CHead e (Bind Abbr)
69 u0)) \to (pc3 c0 t5 t0))))) (\lambda (t5: T).(\lambda (H4: (subst0 i0 u0 t2
70 t5)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
71 u0))).(pc3_t t2 c t5 (pc3_s c t5 t2 (pc3_pr2_r c t2 t5 (pr2_delta c e u0 i0
72 H5 t2 t2 (pr0_refl t2) t5 H4))) t0 (pc3_pr2_r c t2 t0 (pr2_delta c d u i H0
73 t2 t3 H1 t0 H2))))))) (\lambda (c0: C).(\lambda (H4: (csubst0 i0 u0 c
74 c0)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
75 u0))).(lt_le_e i i0 (pc3 c0 t2 t0) (\lambda (H6: (lt i i0)).(let H7 \def
76 (csubst0_getl_lt i0 i H6 c c0 u0 H4 (CHead d (Bind Abbr) u) H0) in (or4_ind
77 (getl i c0 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda
78 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
79 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
80 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
81 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
82 u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
83 C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))
84 (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0
85 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
86 C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (ex4_5 B C C T T
87 (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
88 (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
89 (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
90 i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
91 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
92 (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
93 (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))) (pc3 c0 t2 t0) (\lambda (H8:
94 (getl i c0 (CHead d (Bind Abbr) u))).(pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i
95 H8 t2 t3 H1 t0 H2))) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda
96 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
97 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
98 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
99 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
100 u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda
101 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b)
102 u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
103 T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_:
104 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w)))))
105 (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda
106 (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
107 x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda (H11:
108 (subst0 (minus i0 (S i)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0:
109 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
110 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
111 x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
112 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
113 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
114 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
115 x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match
116 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
117 t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
118 (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def
119 (eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x3)) H11 u
120 H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
121 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
122 B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in (ex2_ind T (\lambda
123 (t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
124 i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H20: (subst0 i x3
125 t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
126 H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
127 nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
128 t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0 x t0 (pr2_delta
129 c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
130 u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3 t0 u i H2 x3
131 u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4
132 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq
133 C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b:
134 B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
135 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
136 (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
137 (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
138 Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
139 (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
140 B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
141 i)) u0 e1 e2))))) (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda
142 (x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
143 x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
144 x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H12 \def
145 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
146 [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
147 Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda
148 (e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
149 Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
150 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
151 u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
152 C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
153 (CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
154 x3) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let
155 H17 \def (eq_ind_r T x3 (\lambda (t5: T).(getl i c0 (CHead x2 (Bind x0) t5)))
156 H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
157 i0 (S i)) u0 c3 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
158 B).(getl i c0 (CHead x2 (Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0
159 (pr2_delta c0 x2 u i H19 t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8))
160 (\lambda (H8: (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
161 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
162 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
163 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
164 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
165 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
166 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
167 e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
168 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
169 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
170 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
171 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
172 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
173 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
174 (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
175 (x3: T).(\lambda (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
176 x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
177 x4))).(\lambda (H11: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12:
178 (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0:
179 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
180 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
181 x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
182 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
183 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
184 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
185 x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
186 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
187 t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
188 (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
189 (eq_ind_r T x3 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x4)) H11 u
190 H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
191 i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
192 B).(getl i c0 (CHead x2 (Bind b) x4))) H10 Abbr H16) in (ex2_ind T (\lambda
193 (t5: T).(subst0 i x4 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
194 i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x4
195 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
196 H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
197 nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
198 t2 (pr2_delta c0 x2 x4 i H20 t2 t3 H1 x H21) t0 (pc3_pr2_x c0 x t0 (pr2_delta
199 c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
200 u0) H5) t0 t0 (pr0_refl t0) x H23))))))) (subst0_subst0_back t3 t0 u i H2 x4
201 u0 (minus i0 (S i)) H18)))))))) H14)) H13))))))))))) H8)) H7))) (\lambda (H6:
202 (le i0 i)).(pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i (csubst0_getl_ge i0 i H6 c
203 c0 u0 H4 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0 H2)))))))) (\lambda (t5:
204 T).(\lambda (H4: (subst0 i0 u0 t2 t5)).(\lambda (c0: C).(\lambda (H5:
205 (csubst0 i0 u0 c c0)).(\lambda (e: C).(\lambda (H6: (getl i0 c (CHead e (Bind
206 Abbr) u0))).(lt_le_e i i0 (pc3 c0 t5 t0) (\lambda (H7: (lt i i0)).(let H8
207 \def (csubst0_getl_lt i0 i H7 c c0 u0 H5 (CHead d (Bind Abbr) u) H0) in
208 (or4_ind (getl i c0 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b:
209 B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind
210 Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0:
211 C).(\lambda (_: T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w))))))
212 (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
213 (minus i0 (S i)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1:
214 C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
215 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
216 (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1:
217 C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
218 (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
219 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
220 u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
221 T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
222 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
223 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
224 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))
225 (pc3 c0 t5 t0) (\lambda (H9: (getl i c0 (CHead d (Bind Abbr) u))).(pc3_pr2_u2
226 c0 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5
227 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_r c0 t2
228 t0 (pr2_delta c0 d u i H9 t2 t3 H1 t0 H2)))) (\lambda (H9: (ex3_4 B C T T
229 (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C
230 (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda
231 (e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w))))))
232 (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
233 (minus i0 (S i)) u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda
234 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
235 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
236 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
237 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
238 u0 u1 w))))) (pc3 c0 t5 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2:
239 T).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1
240 (Bind x0) x2))).(\lambda (H11: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda
241 (H12: (subst0 (minus i0 (S i)) u0 x2 x3)).(let H13 \def (f_equal C C (\lambda
242 (e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow
243 d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind
244 x0) x2) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C
245 return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
246 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
247 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
248 x1 (Bind x0) x2) H10) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
249 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
250 t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
251 (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
252 (eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x3)) H12 u
253 H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
254 (Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
255 B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in (ex2_ind T (\lambda
256 (t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
257 i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x3
258 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
259 H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
260 nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u2 c0
261 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5
262 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_u c0 x t2
263 (pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t0 (pc3_pr2_x c0 x t0 (pr2_delta c0
264 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
265 H6) t0 t0 (pr0_refl t0) x H23)))))))) (subst0_subst0_back t3 t0 u i H2 x3 u0
266 (minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex3_4 B C
267 C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
268 (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
269 (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b)
270 u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
271 T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
272 B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
273 Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
274 (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
275 B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
276 i)) u0 e1 e2))))) (pc3 c0 t5 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda
277 (x2: C).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
278 x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
279 x3))).(\lambda (H12: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def
280 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
281 [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
282 Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H14 \def (f_equal C B (\lambda
283 (e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
284 Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
285 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
286 u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
287 C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
288 (CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
289 x3) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let
290 H18 \def (eq_ind_r T x3 (\lambda (t6: T).(getl i c0 (CHead x2 (Bind x0) t6)))
291 H11 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
292 i0 (S i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
293 B).(getl i c0 (CHead x2 (Bind b) u))) H18 Abbr H16) in (pc3_pr2_u2 c0 t2 t5
294 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
295 (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_r c0 t2 t0
296 (pr2_delta c0 x2 u i H20 t2 t3 H1 t0 H2))))))))) H14)) H13))))))))) H9))
297 (\lambda (H9: (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
298 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
299 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
300 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
301 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
302 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
303 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
304 e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
305 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
306 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
307 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
308 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
309 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
310 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
311 (pc3 c0 t5 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
312 (x3: T).(\lambda (x4: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
313 x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
314 x4))).(\lambda (H12: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13:
315 (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0:
316 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
317 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
318 x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0: C).(match e0 in C
319 return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
320 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
321 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
322 x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T (\lambda (e0: C).(match
323 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
324 t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
325 (\lambda (H17: (eq B Abbr x0)).(\lambda (H18: (eq C d x1)).(let H19 \def
326 (eq_ind_r T x3 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x4)) H12 u
327 H16) in (let H20 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
328 i)) u0 c3 x2)) H13 d H18) in (let H21 \def (eq_ind_r B x0 (\lambda (b:
329 B).(getl i c0 (CHead x2 (Bind b) x4))) H11 Abbr H17) in (ex2_ind T (\lambda
330 (t6: T).(subst0 i x4 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
331 i)) i)) u0 t0 t6)) (pc3 c0 t5 t0) (\lambda (x: T).(\lambda (H22: (subst0 i x4
332 t3 x)).(\lambda (H23: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
333 H24 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
334 nat).(subst0 n u0 t0 x)) H23 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u2 c0
335 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5
336 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4) t0 (pc3_pr2_u c0 x t2
337 (pr2_delta c0 x2 x4 i H21 t2 t3 H1 x H22) t0 (pc3_pr2_x c0 x t0 (pr2_delta c0
338 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
339 H6) t0 t0 (pr0_refl t0) x H24)))))))) (subst0_subst0_back t3 t0 u i H2 x4 u0
340 (minus i0 (S i)) H19)))))))) H15)) H14))))))))))) H9)) H8))) (\lambda (H7:
341 (le i0 i)).(pc3_pr2_u2 c0 t2 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0
342 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t2 t2 (pr0_refl t2) t5 H4)
343 t0 (pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i (csubst0_getl_ge i0 i H7 c c0 u0
344 H5 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0 H2))))))))))) c2 t4
345 H3)))))))))))))))) c1 t1 t H)))).
347 theorem pc3_pr2_fsubst0_back:
348 \forall (c1: C).(\forall (t: T).(\forall (t1: T).((pr2 c1 t t1) \to (\forall
349 (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
350 t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
353 \lambda (c1: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pr2 c1 t
354 t1)).(pr2_ind (\lambda (c: C).(\lambda (t0: T).(\lambda (t2: T).(\forall (i:
355 nat).(\forall (u: T).(\forall (c2: C).(\forall (t3: T).((fsubst0 i u c t2 c2
356 t3) \to (\forall (e: C).((getl i c (CHead e (Bind Abbr) u)) \to (pc3 c2 t0
357 t3))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H0:
358 (pr0 t2 t3)).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t0:
359 T).(\lambda (H1: (fsubst0 i u c t3 c2 t0)).(fsubst0_ind i u c t3 (\lambda
360 (c0: C).(\lambda (t4: T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u))
361 \to (pc3 c0 t2 t4))))) (\lambda (t4: T).(\lambda (H2: (subst0 i u t3
362 t4)).(\lambda (e: C).(\lambda (H3: (getl i c (CHead e (Bind Abbr)
363 u))).(pc3_pr2_u c t3 t2 (pr2_free c t2 t3 H0) t4 (pc3_pr2_r c t3 t4
364 (pr2_delta c e u i H3 t3 t3 (pr0_refl t3) t4 H2))))))) (\lambda (c0:
365 C).(\lambda (_: (csubst0 i u c c0)).(\lambda (e: C).(\lambda (_: (getl i c
366 (CHead e (Bind Abbr) u))).(pc3_pr2_r c0 t2 t3 (pr2_free c0 t2 t3 H0))))))
367 (\lambda (t4: T).(\lambda (H2: (subst0 i u t3 t4)).(\lambda (c0: C).(\lambda
368 (H3: (csubst0 i u c c0)).(\lambda (e: C).(\lambda (H4: (getl i c (CHead e
369 (Bind Abbr) u))).(pc3_pr2_u c0 t3 t2 (pr2_free c0 t2 t3 H0) t4 (pc3_pr2_r c0
370 t3 t4 (pr2_delta c0 e u i (csubst0_getl_ge i i (le_n i) c c0 u H3 (CHead e
371 (Bind Abbr) u) H4) t3 t3 (pr0_refl t3) t4 H2))))))))) c2 t0 H1))))))))))
372 (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
373 (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t2: T).(\lambda (t3:
374 T).(\lambda (H1: (pr0 t2 t3)).(\lambda (t0: T).(\lambda (H2: (subst0 i u t3
375 t0)).(\lambda (i0: nat).(\lambda (u0: T).(\lambda (c2: C).(\lambda (t4:
376 T).(\lambda (H3: (fsubst0 i0 u0 c t0 c2 t4)).(fsubst0_ind i0 u0 c t0 (\lambda
377 (c0: C).(\lambda (t5: T).(\forall (e: C).((getl i0 c (CHead e (Bind Abbr)
378 u0)) \to (pc3 c0 t2 t5))))) (\lambda (t5: T).(\lambda (H4: (subst0 i0 u0 t0
379 t5)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
380 u0))).(pc3_t t3 c t2 (pc3_pr3_r c t2 t3 (pr3_pr2 c t2 t3 (pr2_free c t2 t3
381 H1))) t5 (pc3_pr3_r c t3 t5 (pr3_sing c t0 t3 (pr2_delta c d u i H0 t3 t3
382 (pr0_refl t3) t0 H2) t5 (pr3_pr2 c t0 t5 (pr2_delta c e u0 i0 H5 t0 t0
383 (pr0_refl t0) t5 H4))))))))) (\lambda (c0: C).(\lambda (H4: (csubst0 i0 u0 c
384 c0)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
385 u0))).(lt_le_e i i0 (pc3 c0 t2 t0) (\lambda (H6: (lt i i0)).(let H7 \def
386 (csubst0_getl_lt i0 i H6 c c0 u0 H4 (CHead d (Bind Abbr) u) H0) in (or4_ind
387 (getl i c0 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda
388 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
389 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
390 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
391 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
392 u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
393 C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))
394 (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0
395 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
396 C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (ex4_5 B C C T T
397 (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
398 (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
399 (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
400 i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
401 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
402 (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
403 (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))) (pc3 c0 t2 t0) (\lambda (H8:
404 (getl i c0 (CHead d (Bind Abbr) u))).(pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i
405 H8 t2 t3 H1 t0 H2))) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda
406 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
407 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
408 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
409 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
410 u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda
411 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b)
412 u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
413 T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_:
414 C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w)))))
415 (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda
416 (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
417 x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda (H11:
418 (subst0 (minus i0 (S i)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0:
419 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
420 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
421 x2) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
422 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
423 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
424 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
425 x1 (Bind x0) x2) H9) in ((let H14 \def (f_equal C T (\lambda (e0: C).(match
426 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
427 t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
428 (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let H17 \def
429 (eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x3)) H11 u
430 H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
431 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
432 B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in (ex2_ind T (\lambda
433 (t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
434 i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H20: (subst0 i x3
435 t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
436 H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
437 nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
438 t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0 x t0 (pr2_delta
439 c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
440 u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3 t0 u i H2 x3
441 u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda (H8: (ex3_4
442 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq
443 C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b:
444 B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
445 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
446 (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
447 (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
448 Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
449 (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
450 B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
451 i)) u0 e1 e2))))) (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda
452 (x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
453 x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
454 x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H12 \def
455 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
456 [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
457 Abbr) u) (CHead x1 (Bind x0) x3) H9) in ((let H13 \def (f_equal C B (\lambda
458 (e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
459 Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
460 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
461 u) (CHead x1 (Bind x0) x3) H9) in ((let H14 \def (f_equal C T (\lambda (e0:
462 C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
463 (CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
464 x3) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let
465 H17 \def (eq_ind_r T x3 (\lambda (t5: T).(getl i c0 (CHead x2 (Bind x0) t5)))
466 H10 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
467 i0 (S i)) u0 c3 x2)) H11 d H16) in (let H19 \def (eq_ind_r B x0 (\lambda (b:
468 B).(getl i c0 (CHead x2 (Bind b) u))) H17 Abbr H15) in (pc3_pr2_r c0 t2 t0
469 (pr2_delta c0 x2 u i H19 t2 t3 H1 t0 H2)))))))) H13)) H12))))))))) H8))
470 (\lambda (H8: (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
471 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
472 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
473 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
474 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
475 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
476 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
477 e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
478 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
479 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
480 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
481 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
482 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
483 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
484 (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
485 (x3: T).(\lambda (x4: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
486 x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
487 x4))).(\lambda (H11: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H12:
488 (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def (f_equal C C (\lambda (e0:
489 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
490 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
491 x3) H9) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
492 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
493 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
494 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
495 x1 (Bind x0) x3) H9) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
496 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
497 t5) \Rightarrow t5])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H9) in
498 (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
499 (eq_ind_r T x3 (\lambda (t5: T).(subst0 (minus i0 (S i)) u0 t5 x4)) H11 u
500 H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
501 i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
502 B).(getl i c0 (CHead x2 (Bind b) x4))) H10 Abbr H16) in (ex2_ind T (\lambda
503 (t5: T).(subst0 i x4 t3 t5)) (\lambda (t5: T).(subst0 (S (plus (minus i0 (S
504 i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x4
505 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
506 H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
507 nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H6)) in (pc3_pr2_u c0 x
508 t2 (pr2_delta c0 x2 x4 i H20 t2 t3 H1 x H21) t0 (pc3_pr2_x c0 x t0 (pr2_delta
509 c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead e (Bind Abbr)
510 u0) H5) t0 t0 (pr0_refl t0) x H23))))))) (subst0_subst0_back t3 t0 u i H2 x4
511 u0 (minus i0 (S i)) H18)))))))) H14)) H13))))))))))) H8)) H7))) (\lambda (H6:
512 (le i0 i)).(pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i (csubst0_getl_ge i0 i H6 c
513 c0 u0 H4 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0 H2)))))))) (\lambda (t5:
514 T).(\lambda (H4: (subst0 i0 u0 t0 t5)).(\lambda (c0: C).(\lambda (H5:
515 (csubst0 i0 u0 c c0)).(\lambda (e: C).(\lambda (H6: (getl i0 c (CHead e (Bind
516 Abbr) u0))).(lt_le_e i i0 (pc3 c0 t2 t5) (\lambda (H7: (lt i i0)).(let H8
517 \def (csubst0_getl_lt i0 i H7 c c0 u0 H5 (CHead d (Bind Abbr) u) H0) in
518 (or4_ind (getl i c0 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b:
519 B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind
520 Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0:
521 C).(\lambda (_: T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w))))))
522 (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
523 (minus i0 (S i)) u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1:
524 C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
525 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
526 (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1:
527 C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
528 (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
529 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
530 u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
531 T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
532 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
533 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
534 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))
535 (pc3 c0 t2 t5) (\lambda (H9: (getl i c0 (CHead d (Bind Abbr) u))).(pc3_pr2_u
536 c0 t3 t2 (pr2_free c0 t2 t3 H1) t5 (pc3_pr3_r c0 t3 t5 (pr3_sing c0 t0 t3
537 (pr2_delta c0 d u i H9 t3 t3 (pr0_refl t3) t0 H2) t5 (pr3_pr2 c0 t0 t5
538 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
539 (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5 H4)))))) (\lambda (H9: (ex3_4 B C
540 T T (\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C
541 (CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda
542 (e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w))))))
543 (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
544 (minus i0 (S i)) u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda
545 (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
546 e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
547 T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
548 B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
549 u0 u1 w))))) (pc3 c0 t2 t5) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2:
550 T).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1
551 (Bind x0) x2))).(\lambda (H11: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda
552 (H12: (subst0 (minus i0 (S i)) u0 x2 x3)).(let H13 \def (f_equal C C (\lambda
553 (e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow
554 d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind
555 x0) x2) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 in C
556 return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
557 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
558 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
559 x1 (Bind x0) x2) H10) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match
560 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
561 t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H10) in
562 (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def
563 (eq_ind_r T x2 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x3)) H12 u
564 H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(getl i c0 (CHead c3
565 (Bind x0) x3))) H11 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
566 B).(getl i c0 (CHead d (Bind b) x3))) H19 Abbr H16) in (ex2_ind T (\lambda
567 (t6: T).(subst0 i x3 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
568 i)) i)) u0 t0 t6)) (pc3 c0 t2 t5) (\lambda (x: T).(\lambda (H21: (subst0 i x3
569 t3 x)).(\lambda (H22: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
570 H23 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
571 nat).(subst0 n u0 t0 x)) H22 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u c0 x
572 t2 (pr2_delta c0 d x3 i H20 t2 t3 H1 x H21) t5 (pc3_pr2_u2 c0 t0 x (pr2_delta
573 c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr)
574 u0) H6) t0 t0 (pr0_refl t0) x H23) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0
575 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6)
576 t0 t0 (pr0_refl t0) t5 H4)))))))) (subst0_subst0_back t3 t0 u i H2 x3 u0
577 (minus i0 (S i)) H18)))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex3_4 B C
578 C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
579 (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
580 (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b)
581 u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
582 T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda (b:
583 B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
584 Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
585 (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
586 B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
587 i)) u0 e1 e2))))) (pc3 c0 t2 t5) (\lambda (x0: B).(\lambda (x1: C).(\lambda
588 (x2: C).(\lambda (x3: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
589 x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
590 x3))).(\lambda (H12: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H13 \def
591 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
592 [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind
593 Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H14 \def (f_equal C B (\lambda
594 (e0: C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
595 Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
596 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr)
597 u) (CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
598 C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
599 (CHead _ _ t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
600 x3) H10) in (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq C d x1)).(let
601 H18 \def (eq_ind_r T x3 (\lambda (t6: T).(getl i c0 (CHead x2 (Bind x0) t6)))
602 H11 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus
603 i0 (S i)) u0 c3 x2)) H12 d H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b:
604 B).(getl i c0 (CHead x2 (Bind b) u))) H18 Abbr H16) in (pc3_pr2_u c0 t0 t2
605 (pr2_delta c0 x2 u i H20 t2 t3 H1 t0 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0
606 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0)
607 H6) t0 t0 (pr0_refl t0) t5 H4))))))))) H14)) H13))))))))) H9)) (\lambda (H9:
608 (ex4_5 B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
609 (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b)
610 u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
611 T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
612 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
613 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
614 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1
615 e2)))))))).(ex4_5_ind B C C T T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
616 C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1
617 (Bind b) u1))))))) (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda
618 (_: T).(\lambda (w: T).(getl i c0 (CHead e2 (Bind b) w))))))) (\lambda (_:
619 B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
620 (minus i0 (S i)) u0 u1 w)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
621 C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))
622 (pc3 c0 t2 t5) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: C).(\lambda
623 (x3: T).(\lambda (x4: T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead
624 x1 (Bind x0) x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0)
625 x4))).(\lambda (H12: (subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13:
626 (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0:
627 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
628 (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
629 x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0: C).(match e0 in C
630 return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
631 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
632 \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
633 x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T (\lambda (e0: C).(match
634 e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
635 t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
636 (\lambda (H17: (eq B Abbr x0)).(\lambda (H18: (eq C d x1)).(let H19 \def
637 (eq_ind_r T x3 (\lambda (t6: T).(subst0 (minus i0 (S i)) u0 t6 x4)) H12 u
638 H16) in (let H20 \def (eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S
639 i)) u0 c3 x2)) H13 d H18) in (let H21 \def (eq_ind_r B x0 (\lambda (b:
640 B).(getl i c0 (CHead x2 (Bind b) x4))) H11 Abbr H17) in (ex2_ind T (\lambda
641 (t6: T).(subst0 i x4 t3 t6)) (\lambda (t6: T).(subst0 (S (plus (minus i0 (S
642 i)) i)) u0 t0 t6)) (pc3 c0 t2 t5) (\lambda (x: T).(\lambda (H22: (subst0 i x4
643 t3 x)).(\lambda (H23: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
644 H24 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i)) (\lambda (n:
645 nat).(subst0 n u0 t0 x)) H23 i0 (lt_plus_minus_r i i0 H7)) in (pc3_pr2_u c0 x
646 t2 (pr2_delta c0 x2 x4 i H21 t2 t3 H1 x H22) t5 (pc3_pr2_u2 c0 t0 x
647 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
648 (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) x H24) t5 (pc3_pr2_r c0 t0 t5
649 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H5 (CHead e
650 (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5 H4)))))))) (subst0_subst0_back t3
651 t0 u i H2 x4 u0 (minus i0 (S i)) H19)))))))) H15)) H14))))))))))) H9)) H8)))
652 (\lambda (H7: (le i0 i)).(pc3_pr2_u c0 t0 t2 (pr2_delta c0 d u i
653 (csubst0_getl_ge i0 i H7 c c0 u0 H5 (CHead d (Bind Abbr) u) H0) t2 t3 H1 t0
654 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n
655 i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0) t5
656 H4))))))))))) c2 t4 H3)))))))))))))))) c1 t t1 H)))).
659 \forall (c1: C).(\forall (t1: T).(\forall (t: T).((pc3 c1 t1 t) \to (\forall
660 (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t2: T).((fsubst0 i u c1
661 t1 c2 t2) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3
664 \lambda (c1: C).(\lambda (t1: T).(\lambda (t: T).(\lambda (H: (pc3 c1 t1
665 t)).(pc3_ind_left c1 (\lambda (t0: T).(\lambda (t2: T).(\forall (i:
666 nat).(\forall (u: T).(\forall (c2: C).(\forall (t3: T).((fsubst0 i u c1 t0 c2
667 t3) \to (\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3 c2 t3
668 t2)))))))))) (\lambda (t0: T).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2:
669 C).(\lambda (t2: T).(\lambda (H0: (fsubst0 i u c1 t0 c2 t2)).(fsubst0_ind i u
670 c1 t0 (\lambda (c: C).(\lambda (t3: T).(\forall (e: C).((getl i c1 (CHead e
671 (Bind Abbr) u)) \to (pc3 c t3 t0))))) (\lambda (t3: T).(\lambda (H1: (subst0
672 i u t0 t3)).(\lambda (e: C).(\lambda (H2: (getl i c1 (CHead e (Bind Abbr)
673 u))).(pc3_pr2_x c1 t3 t0 (pr2_delta c1 e u i H2 t0 t0 (pr0_refl t0) t3
674 H1)))))) (\lambda (c0: C).(\lambda (_: (csubst0 i u c1 c0)).(\lambda (e:
675 C).(\lambda (_: (getl i c1 (CHead e (Bind Abbr) u))).(pc3_refl c0 t0)))))
676 (\lambda (t3: T).(\lambda (H1: (subst0 i u t0 t3)).(\lambda (c0: C).(\lambda
677 (H2: (csubst0 i u c1 c0)).(\lambda (e: C).(\lambda (H3: (getl i c1 (CHead e
678 (Bind Abbr) u))).(pc3_pr2_x c0 t3 t0 (pr2_delta c0 e u i (csubst0_getl_ge i i
679 (le_n i) c1 c0 u H2 (CHead e (Bind Abbr) u) H3) t0 t0 (pr0_refl t0) t3
680 H1)))))))) c2 t2 H0))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda (H0:
681 (pr2 c1 t0 t2)).(\lambda (t3: T).(\lambda (H1: (pc3 c1 t2 t3)).(\lambda (H2:
682 ((\forall (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t4:
683 T).((fsubst0 i u c1 t2 c2 t4) \to (\forall (e: C).((getl i c1 (CHead e (Bind
684 Abbr) u)) \to (pc3 c2 t4 t3)))))))))).(\lambda (i: nat).(\lambda (u:
685 T).(\lambda (c2: C).(\lambda (t4: T).(\lambda (H3: (fsubst0 i u c1 t0 c2
686 t4)).(fsubst0_ind i u c1 t0 (\lambda (c: C).(\lambda (t5: T).(\forall (e:
687 C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3 c t5 t3))))) (\lambda (t5:
688 T).(\lambda (H4: (subst0 i u t0 t5)).(\lambda (e: C).(\lambda (H5: (getl i c1
689 (CHead e (Bind Abbr) u))).(pc3_t t2 c1 t5 (pc3_pr2_fsubst0 c1 t0 t2 H0 i u c1
690 t5 (fsubst0_snd i u c1 t0 t5 H4) e H5) t3 H1))))) (\lambda (c0: C).(\lambda
691 (H4: (csubst0 i u c1 c0)).(\lambda (e: C).(\lambda (H5: (getl i c1 (CHead e
692 (Bind Abbr) u))).(pc3_t t2 c0 t0 (pc3_pr2_fsubst0 c1 t0 t2 H0 i u c0 t0
693 (fsubst0_fst i u c1 t0 c0 H4) e H5) t3 (H2 i u c0 t2 (fsubst0_fst i u c1 t2
694 c0 H4) e H5)))))) (\lambda (t5: T).(\lambda (H4: (subst0 i u t0 t5)).(\lambda
695 (c0: C).(\lambda (H5: (csubst0 i u c1 c0)).(\lambda (e: C).(\lambda (H6:
696 (getl i c1 (CHead e (Bind Abbr) u))).(pc3_t t2 c0 t5 (pc3_pr2_fsubst0 c1 t0
697 t2 H0 i u c0 t5 (fsubst0_both i u c1 t0 t5 H4 c0 H5) e H6) t3 (H2 i u c0 t2
698 (fsubst0_fst i u c1 t2 c0 H5) e H6)))))))) c2 t4 H3)))))))))))) (\lambda (t0:
699 T).(\lambda (t2: T).(\lambda (H0: (pr2 c1 t0 t2)).(\lambda (t3: T).(\lambda
700 (H1: (pc3 c1 t0 t3)).(\lambda (H2: ((\forall (i: nat).(\forall (u:
701 T).(\forall (c2: C).(\forall (t4: T).((fsubst0 i u c1 t0 c2 t4) \to (\forall
702 (e: C).((getl i c1 (CHead e (Bind Abbr) u)) \to (pc3 c2 t4
703 t3)))))))))).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t4:
704 T).(\lambda (H3: (fsubst0 i u c1 t2 c2 t4)).(fsubst0_ind i u c1 t2 (\lambda
705 (c: C).(\lambda (t5: T).(\forall (e: C).((getl i c1 (CHead e (Bind Abbr) u))
706 \to (pc3 c t5 t3))))) (\lambda (t5: T).(\lambda (H4: (subst0 i u t2
707 t5)).(\lambda (e: C).(\lambda (H5: (getl i c1 (CHead e (Bind Abbr)
708 u))).(pc3_t t0 c1 t5 (pc3_s c1 t5 t0 (pc3_pr2_fsubst0_back c1 t0 t2 H0 i u c1
709 t5 (fsubst0_snd i u c1 t2 t5 H4) e H5)) t3 H1))))) (\lambda (c0: C).(\lambda
710 (H4: (csubst0 i u c1 c0)).(\lambda (e: C).(\lambda (H5: (getl i c1 (CHead e
711 (Bind Abbr) u))).(pc3_t t0 c0 t2 (pc3_s c0 t2 t0 (pc3_pr2_fsubst0_back c1 t0
712 t2 H0 i u c0 t2 (fsubst0_fst i u c1 t2 c0 H4) e H5)) t3 (H2 i u c0 t0
713 (fsubst0_fst i u c1 t0 c0 H4) e H5)))))) (\lambda (t5: T).(\lambda (H4:
714 (subst0 i u t2 t5)).(\lambda (c0: C).(\lambda (H5: (csubst0 i u c1
715 c0)).(\lambda (e: C).(\lambda (H6: (getl i c1 (CHead e (Bind Abbr)
716 u))).(pc3_t t0 c0 t5 (pc3_s c0 t5 t0 (pc3_pr2_fsubst0_back c1 t0 t2 H0 i u c0
717 t5 (fsubst0_both i u c1 t2 t5 H4 c0 H5) e H6)) t3 (H2 i u c0 t0 (fsubst0_fst
718 i u c1 t0 c0 H5) e H6)))))))) c2 t4 H3)))))))))))) t1 t H)))).
projects / helm.git / blob