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