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