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-1/csubc/defs.ma".
19 theorem csubc_gen_sort_l:
20 \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g (CSort n) x) \to
23 \lambda (g: G).(\lambda (x: C).(\lambda (n: nat).(\lambda (H: (csubc g
24 (CSort n) x)).(insert_eq C (CSort n) (\lambda (c: C).(csubc g c x)) (\lambda
25 (c: C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (csubc g y x)).(csubc_ind g
26 (\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n)) \to (eq C c0 c))))
27 (\lambda (n0: nat).(\lambda (H1: (eq C (CSort n0) (CSort n))).(let H2 \def
28 (f_equal C nat (\lambda (e: C).(match e in C return (\lambda (_: C).nat) with
29 [(CSort n1) \Rightarrow n1 | (CHead _ _ _) \Rightarrow n0])) (CSort n0)
30 (CSort n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(eq C (CSort n1) (CSort
31 n1))) (refl_equal C (CSort n)) n0 H2)))) (\lambda (c1: C).(\lambda (c2:
32 C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c1 (CSort n)) \to (eq C
33 c2 c1)))).(\lambda (k: K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c1 k v)
34 (CSort n))).(let H4 \def (eq_ind C (CHead c1 k v) (\lambda (ee: C).(match ee
35 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead
36 _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (eq C (CHead c2 k v)
37 (CHead c1 k v)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
38 (csubc g c1 c2)).(\lambda (_: (((eq C c1 (CSort n)) \to (eq C c2
39 c1)))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
40 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u1) (CSort
41 n))).(let H5 \def (eq_ind C (CHead c1 (Bind Void) u1) (\lambda (ee: C).(match
42 ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
43 (CHead _ _ _) \Rightarrow True])) I (CSort n) H4) in (False_ind (eq C (CHead
44 c2 (Bind b) u2) (CHead c1 (Bind Void) u1)) H5))))))))))) (\lambda (c1:
45 C).(\lambda (c2: C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c1
46 (CSort n)) \to (eq C c2 c1)))).(\lambda (v: T).(\lambda (a: A).(\lambda (_:
47 (sc3 g (asucc g a) c1 v)).(\lambda (w: T).(\lambda (_: (sc3 g a c2
48 w)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) v) (CSort n))).(let H6 \def
49 (eq_ind C (CHead c1 (Bind Abst) v) (\lambda (ee: C).(match ee in C return
50 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _)
51 \Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c2 (Bind Abbr)
52 w) (CHead c1 (Bind Abst) v)) H6)))))))))))) y x H0))) H)))).
57 theorem csubc_gen_head_l:
58 \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (k:
59 K).((csubc g (CHead c1 k v) x) \to (or3 (ex2 C (\lambda (c2: C).(eq C x
60 (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A (\lambda (_:
61 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c2:
62 C).(\lambda (w: T).(\lambda (_: A).(eq C x (CHead c2 (Bind Abbr) w)))))
63 (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c2)))) (\lambda
64 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
65 (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T
66 (\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(eq C x (CHead c2 (Bind b)
67 v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
68 Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
69 Void))))) (\lambda (_: B).(\lambda (c2: C).(\lambda (_: T).(csubc g c1
72 \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (k:
73 K).(\lambda (H: (csubc g (CHead c1 k v) x)).(insert_eq C (CHead c1 k v)
74 (\lambda (c: C).(csubc g c x)) (\lambda (_: C).(or3 (ex2 C (\lambda (c2:
75 C).(eq C x (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A
76 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
77 (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C x (CHead c2 (Bind
78 Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
79 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
80 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w)))))
81 (ex4_3 B C T (\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(eq C x (CHead
82 c2 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k
83 (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
84 Void))))) (\lambda (_: B).(\lambda (c2: C).(\lambda (_: T).(csubc g c1
85 c2))))))) (\lambda (y: C).(\lambda (H0: (csubc g y x)).(csubc_ind g (\lambda
86 (c: C).(\lambda (c0: C).((eq C c (CHead c1 k v)) \to (or3 (ex2 C (\lambda
87 (c2: C).(eq C c0 (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C
88 T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
89 (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C c0 (CHead c2 (Bind
90 Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
91 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
92 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w)))))
93 (ex4_3 B C T (\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(eq C c0
94 (CHead c2 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
95 T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
96 T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c2: C).(\lambda (_:
97 T).(csubc g c1 c2))))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n)
98 (CHead c1 k v))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee
99 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _
100 _ _) \Rightarrow False])) I (CHead c1 k v) H1) in (False_ind (or3 (ex2 C
101 (\lambda (c2: C).(eq C (CSort n) (CHead c2 k v))) (\lambda (c2: C).(csubc g
102 c1 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
103 (Bind Abst))))) (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C (CSort
104 n) (CHead c2 (Bind Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_:
105 A).(csubc g c1 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g
106 (asucc g a) c1 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
107 a c2 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c2: C).(\lambda (v2:
108 T).(eq C (CSort n) (CHead c2 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
109 C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_:
110 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c2:
111 C).(\lambda (_: T).(csubc g c1 c2)))))) H2)))) (\lambda (c0: C).(\lambda (c2:
112 C).(\lambda (H1: (csubc g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k v))
113 \to (or3 (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3:
114 C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
115 (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_:
116 A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_:
117 T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_:
118 T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3: C).(\lambda (w:
119 T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda
120 (c3: C).(\lambda (v2: T).(eq C c2 (CHead c3 (Bind b) v2))))) (\lambda (_:
121 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b:
122 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
123 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1 c3))))))))).(\lambda (k0:
124 K).(\lambda (v0: T).(\lambda (H3: (eq C (CHead c0 k0 v0) (CHead c1 k
125 v))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
126 (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c]))
127 (CHead c0 k0 v0) (CHead c1 k v) H3) in ((let H5 \def (f_equal C K (\lambda
128 (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0
129 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 v0) (CHead c1 k v) H3) in
130 ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
131 C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead
132 c0 k0 v0) (CHead c1 k v) H3) in (\lambda (H7: (eq K k0 k)).(\lambda (H8: (eq
133 C c0 c1)).(eq_ind_r T v (\lambda (t: T).(or3 (ex2 C (\lambda (c3: C).(eq C
134 (CHead c2 k0 t) (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C
135 T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
136 (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C (CHead c2 k0 t) (CHead
137 c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc
138 g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g
139 a) c1 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3
140 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C
141 (CHead c2 k0 t) (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
142 C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_:
143 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
144 C).(\lambda (_: T).(csubc g c1 c3))))))) (eq_ind_r K k (\lambda (k1: K).(or3
145 (ex2 C (\lambda (c3: C).(eq C (CHead c2 k1 v) (CHead c3 k v))) (\lambda (c3:
146 C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
147 (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_:
148 A).(eq C (CHead c2 k1 v) (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
149 C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
150 C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3:
151 C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda
152 (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C (CHead c2 k1 v) (CHead c3
153 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k
154 (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
155 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1
156 c3))))))) (let H9 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 k v))
157 \to (or3 (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3:
158 C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
159 (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_:
160 A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_:
161 T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_:
162 T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3: C).(\lambda (w:
163 T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda
164 (c3: C).(\lambda (v2: T).(eq C c2 (CHead c3 (Bind b) v2))))) (\lambda (_:
165 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b:
166 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
167 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1 c3)))))))) H2 c1 H8) in (let
168 H10 \def (eq_ind C c0 (\lambda (c: C).(csubc g c c2)) H1 c1 H8) in
169 (or3_intro0 (ex2 C (\lambda (c3: C).(eq C (CHead c2 k v) (CHead c3 k v)))
170 (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
171 T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w:
172 T).(\lambda (_: A).(eq C (CHead c2 k v) (CHead c3 (Bind Abbr) w))))) (\lambda
173 (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
174 C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3:
175 C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda
176 (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C (CHead c2 k v) (CHead c3 (Bind
177 b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
178 Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
179 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1
180 c3))))) (ex_intro2 C (\lambda (c3: C).(eq C (CHead c2 k v) (CHead c3 k v)))
181 (\lambda (c3: C).(csubc g c1 c3)) c2 (refl_equal C (CHead c2 k v)) H10)))) k0
182 H7) v0 H6)))) H5)) H4))))))))) (\lambda (c0: C).(\lambda (c2: C).(\lambda
183 (H1: (csubc g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k v)) \to (or3 (ex2
184 C (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1
185 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
186 (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2
187 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
188 A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g
189 (asucc g a) c1 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
190 a c3 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2:
191 T).(eq C c2 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
192 C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_:
193 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
194 C).(\lambda (_: T).(csubc g c1 c3))))))))).(\lambda (b: B).(\lambda (H3: (not
195 (eq B b Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead
196 c0 (Bind Void) u1) (CHead c1 k v))).(let H5 \def (f_equal C C (\lambda (e:
197 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
198 (CHead c _ _) \Rightarrow c])) (CHead c0 (Bind Void) u1) (CHead c1 k v) H4)
199 in ((let H6 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
200 (_: C).K) with [(CSort _) \Rightarrow (Bind Void) | (CHead _ k0 _)
201 \Rightarrow k0])) (CHead c0 (Bind Void) u1) (CHead c1 k v) H4) in ((let H7
202 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
203 with [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c0
204 (Bind Void) u1) (CHead c1 k v) H4) in (\lambda (H8: (eq K (Bind Void)
205 k)).(\lambda (H9: (eq C c0 c1)).(let H10 \def (eq_ind C c0 (\lambda (c:
206 C).((eq C c (CHead c1 k v)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c2 (CHead
207 c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_:
208 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
209 C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w)))))
210 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda
211 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
212 (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T
213 (\lambda (b0: B).(\lambda (c3: C).(\lambda (v2: T).(eq C c2 (CHead c3 (Bind
214 b0) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
215 Void))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
216 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1
217 c3)))))))) H2 c1 H9) in (let H11 \def (eq_ind C c0 (\lambda (c: C).(csubc g c
218 c2)) H1 c1 H9) in (let H12 \def (eq_ind_r K k (\lambda (k0: K).((eq C c1
219 (CHead c1 k0 v)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k0 v)))
220 (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
221 T).(\lambda (_: A).(eq K k0 (Bind Abst))))) (\lambda (c3: C).(\lambda (w:
222 T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
223 C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
224 C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3:
225 C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda
226 (b0: B).(\lambda (c3: C).(\lambda (v2: T).(eq C c2 (CHead c3 (Bind b0)
227 v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K k0 (Bind
228 Void))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
229 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1
230 c3)))))))) H10 (Bind Void) H8) in (eq_ind K (Bind Void) (\lambda (k0: K).(or3
231 (ex2 C (\lambda (c3: C).(eq C (CHead c2 (Bind b) u2) (CHead c3 k0 v)))
232 (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
233 T).(\lambda (_: A).(eq K k0 (Bind Abst))))) (\lambda (c3: C).(\lambda (w:
234 T).(\lambda (_: A).(eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w)))))
235 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda
236 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
237 (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T
238 (\lambda (b0: B).(\lambda (c3: C).(\lambda (v2: T).(eq C (CHead c2 (Bind b)
239 u2) (CHead c3 (Bind b0) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
240 T).(eq K k0 (Bind Void))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_:
241 T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_:
242 T).(csubc g c1 c3))))))) (or3_intro2 (ex2 C (\lambda (c3: C).(eq C (CHead c2
243 (Bind b) u2) (CHead c3 (Bind Void) v))) (\lambda (c3: C).(csubc g c1 c3)))
244 (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K (Bind
245 Void) (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C
246 (CHead c2 (Bind b) u2) (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda
247 (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_:
248 T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3: C).(\lambda (w:
249 T).(\lambda (a: A).(sc3 g a c3 w))))) (ex4_3 B C T (\lambda (b0: B).(\lambda
250 (c3: C).(\lambda (v2: T).(eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0)
251 v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K (Bind Void)
252 (Bind Void))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B
253 b0 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1
254 c3))))) (ex4_3_intro B C T (\lambda (b0: B).(\lambda (c3: C).(\lambda (v2:
255 T).(eq C (CHead c2 (Bind b) u2) (CHead c3 (Bind b0) v2))))) (\lambda (_:
256 B).(\lambda (_: C).(\lambda (_: T).(eq K (Bind Void) (Bind Void))))) (\lambda
257 (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_:
258 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c1 c3)))) b c2 u2 (refl_equal C
259 (CHead c2 (Bind b) u2)) (refl_equal K (Bind Void)) H3 H11)) k H8))))))) H6))
260 H5))))))))))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (csubc g c0
261 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k v)) \to (or3 (ex2 C (\lambda (c3:
262 C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A
263 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
264 (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind
265 Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
266 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
267 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))))
268 (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C c2
269 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
270 T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
271 T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_:
272 T).(csubc g c1 c3))))))))).(\lambda (v0: T).(\lambda (a: A).(\lambda (H3:
273 (sc3 g (asucc g a) c0 v0)).(\lambda (w: T).(\lambda (H4: (sc3 g a c2
274 w)).(\lambda (H5: (eq C (CHead c0 (Bind Abst) v0) (CHead c1 k v))).(let H6
275 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
276 with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0
277 (Bind Abst) v0) (CHead c1 k v) H5) in ((let H7 \def (f_equal C K (\lambda (e:
278 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow (Bind
279 Abst) | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 (Bind Abst) v0) (CHead c1
280 k v) H5) in ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return
281 (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
282 t])) (CHead c0 (Bind Abst) v0) (CHead c1 k v) H5) in (\lambda (H9: (eq K
283 (Bind Abst) k)).(\lambda (H10: (eq C c0 c1)).(let H11 \def (eq_ind T v0
284 (\lambda (t: T).(sc3 g (asucc g a) c0 t)) H3 v H8) in (let H12 \def (eq_ind C
285 c0 (\lambda (c: C).(sc3 g (asucc g a) c v)) H11 c1 H10) in (let H13 \def
286 (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 k v)) \to (or3 (ex2 C
287 (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3)))
288 (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind
289 Abst))))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (_: A).(eq C c2 (CHead
290 c3 (Bind Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
291 A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g
292 (asucc g a0) c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3
293 g a0 c3 w0))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2:
294 T).(eq C c2 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
295 C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_:
296 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
297 C).(\lambda (_: T).(csubc g c1 c3)))))))) H2 c1 H10) in (let H14 \def (eq_ind
298 C c0 (\lambda (c: C).(csubc g c c2)) H1 c1 H10) in (let H15 \def (eq_ind_r K
299 k (\lambda (k0: K).((eq C c1 (CHead c1 k0 v)) \to (or3 (ex2 C (\lambda (c3:
300 C).(eq C c2 (CHead c3 k0 v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A
301 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k0 (Bind Abst)))))
302 (\lambda (c3: C).(\lambda (w0: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind
303 Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
304 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0)
305 c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3
306 w0))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C
307 c2 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
308 T).(eq K k0 (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
309 T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_:
310 T).(csubc g c1 c3)))))))) H13 (Bind Abst) H9) in (eq_ind K (Bind Abst)
311 (\lambda (k0: K).(or3 (ex2 C (\lambda (c3: C).(eq C (CHead c2 (Bind Abbr) w)
312 (CHead c3 k0 v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda
313 (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k0 (Bind Abst))))) (\lambda (c3:
314 C).(\lambda (w0: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) w) (CHead c3
315 (Bind Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g
316 c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g
317 a0) c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3
318 w0))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C
319 (CHead c2 (Bind Abbr) w) (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda
320 (_: C).(\lambda (_: T).(eq K k0 (Bind Void))))) (\lambda (b: B).(\lambda (_:
321 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
322 C).(\lambda (_: T).(csubc g c1 c3))))))) (or3_intro1 (ex2 C (\lambda (c3:
323 C).(eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abst) v))) (\lambda (c3:
324 C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
325 (_: A).(eq K (Bind Abst) (Bind Abst))))) (\lambda (c3: C).(\lambda (w0:
326 T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr)
327 w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3))))
328 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0) c1 v))))
329 (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3 w0)))))
330 (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C (CHead
331 c2 (Bind Abbr) w) (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
332 C).(\lambda (_: T).(eq K (Bind Abst) (Bind Void))))) (\lambda (b: B).(\lambda
333 (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
334 C).(\lambda (_: T).(csubc g c1 c3))))) (ex5_3_intro C T A (\lambda (_:
335 C).(\lambda (_: T).(\lambda (_: A).(eq K (Bind Abst) (Bind Abst))))) (\lambda
336 (c3: C).(\lambda (w0: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) w)
337 (CHead c3 (Bind Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
338 A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g
339 (asucc g a0) c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3
340 g a0 c3 w0)))) c2 w a (refl_equal K (Bind Abst)) (refl_equal C (CHead c2
341 (Bind Abbr) w)) H14 H12 H4)) k H9))))))))) H7)) H6)))))))))))) y x H0)))
347 theorem csubc_gen_sort_r:
348 \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g x (CSort n)) \to
349 (eq C x (CSort n)))))
351 \lambda (g: G).(\lambda (x: C).(\lambda (n: nat).(\lambda (H: (csubc g x
352 (CSort n))).(insert_eq C (CSort n) (\lambda (c: C).(csubc g x c)) (\lambda
353 (c: C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (csubc g x y)).(csubc_ind g
354 (\lambda (c: C).(\lambda (c0: C).((eq C c0 (CSort n)) \to (eq C c c0))))
355 (\lambda (n0: nat).(\lambda (H1: (eq C (CSort n0) (CSort n))).(let H2 \def
356 (f_equal C nat (\lambda (e: C).(match e in C return (\lambda (_: C).nat) with
357 [(CSort n1) \Rightarrow n1 | (CHead _ _ _) \Rightarrow n0])) (CSort n0)
358 (CSort n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(eq C (CSort n1) (CSort
359 n1))) (refl_equal C (CSort n)) n0 H2)))) (\lambda (c1: C).(\lambda (c2:
360 C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c2 (CSort n)) \to (eq C
361 c1 c2)))).(\lambda (k: K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c2 k v)
362 (CSort n))).(let H4 \def (eq_ind C (CHead c2 k v) (\lambda (ee: C).(match ee
363 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead
364 _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (eq C (CHead c1 k v)
365 (CHead c2 k v)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
366 (csubc g c1 c2)).(\lambda (_: (((eq C c2 (CSort n)) \to (eq C c1
367 c2)))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
368 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CSort
369 n))).(let H5 \def (eq_ind C (CHead c2 (Bind b) u2) (\lambda (ee: C).(match ee
370 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead
371 _ _ _) \Rightarrow True])) I (CSort n) H4) in (False_ind (eq C (CHead c1
372 (Bind Void) u1) (CHead c2 (Bind b) u2)) H5))))))))))) (\lambda (c1:
373 C).(\lambda (c2: C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c2
374 (CSort n)) \to (eq C c1 c2)))).(\lambda (v: T).(\lambda (a: A).(\lambda (_:
375 (sc3 g (asucc g a) c1 v)).(\lambda (w: T).(\lambda (_: (sc3 g a c2
376 w)).(\lambda (H5: (eq C (CHead c2 (Bind Abbr) w) (CSort n))).(let H6 \def
377 (eq_ind C (CHead c2 (Bind Abbr) w) (\lambda (ee: C).(match ee in C return
378 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _)
379 \Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c1 (Bind Abst)
380 v) (CHead c2 (Bind Abbr) w)) H6)))))))))))) x y H0))) H)))).
385 theorem csubc_gen_head_r:
386 \forall (g: G).(\forall (c2: C).(\forall (x: C).(\forall (w: T).(\forall (k:
387 K).((csubc g x (CHead c2 k w)) \to (or3 (ex2 C (\lambda (c1: C).(eq C x
388 (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A (\lambda (_:
389 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c1:
390 C).(\lambda (v: T).(\lambda (_: A).(eq C x (CHead c1 (Bind Abst) v)))))
391 (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c2)))) (\lambda
392 (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
393 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T
394 (\lambda (_: B).(\lambda (c1: C).(\lambda (v1: T).(eq C x (CHead c1 (Bind
395 Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
396 b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void)))))
397 (\lambda (_: B).(\lambda (c1: C).(\lambda (_: T).(csubc g c1 c2)))))))))))
399 \lambda (g: G).(\lambda (c2: C).(\lambda (x: C).(\lambda (w: T).(\lambda (k:
400 K).(\lambda (H: (csubc g x (CHead c2 k w))).(insert_eq C (CHead c2 k w)
401 (\lambda (c: C).(csubc g x c)) (\lambda (_: C).(or3 (ex2 C (\lambda (c1:
402 C).(eq C x (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A
403 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
404 (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C x (CHead c1 (Bind
405 Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
406 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1
407 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))
408 (ex4_3 B C T (\lambda (_: B).(\lambda (c1: C).(\lambda (v1: T).(eq C x (CHead
409 c1 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(eq K
410 k (Bind b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
411 Void))))) (\lambda (_: B).(\lambda (c1: C).(\lambda (_: T).(csubc g c1
412 c2))))))) (\lambda (y: C).(\lambda (H0: (csubc g x y)).(csubc_ind g (\lambda
413 (c: C).(\lambda (c0: C).((eq C c0 (CHead c2 k w)) \to (or3 (ex2 C (\lambda
414 (c1: C).(eq C c (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C
415 T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
416 (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C c (CHead c1 (Bind
417 Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
418 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1
419 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))
420 (ex4_3 B C T (\lambda (_: B).(\lambda (c1: C).(\lambda (v1: T).(eq C c (CHead
421 c1 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(eq K
422 k (Bind b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b
423 Void))))) (\lambda (_: B).(\lambda (c1: C).(\lambda (_: T).(csubc g c1
424 c2))))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead c2 k
425 w))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
426 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
427 \Rightarrow False])) I (CHead c2 k w) H1) in (False_ind (or3 (ex2 C (\lambda
428 (c1: C).(eq C (CSort n) (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2)))
429 (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind
430 Abbr))))) (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C (CSort n)
431 (CHead c1 (Bind Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_:
432 A).(csubc g c1 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g
433 (asucc g a) c1 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a
434 c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda (c1: C).(\lambda (v1: T).(eq
435 C (CSort n) (CHead c1 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_:
436 C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b: B).(\lambda (_:
437 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c1:
438 C).(\lambda (_: T).(csubc g c1 c2)))))) H2)))) (\lambda (c1: C).(\lambda (c0:
439 C).(\lambda (H1: (csubc g c1 c0)).(\lambda (H2: (((eq C c0 (CHead c2 k w))
440 \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3:
441 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
442 (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v: T).(\lambda (_:
443 A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3: C).(\lambda (_:
444 T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v:
445 T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_: C).(\lambda (_:
446 T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda
447 (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b:
448 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
449 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
450 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))))).(\lambda (k0:
451 K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c0 k0 v) (CHead c2 k w))).(let
452 H4 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
453 with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0
454 v) (CHead c2 k w) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e
455 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1
456 _) \Rightarrow k1])) (CHead c0 k0 v) (CHead c2 k w) H3) in ((let H6 \def
457 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
458 [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 v)
459 (CHead c2 k w) H3) in (\lambda (H7: (eq K k0 k)).(\lambda (H8: (eq C c0
460 c2)).(eq_ind_r T w (\lambda (t: T).(or3 (ex2 C (\lambda (c3: C).(eq C (CHead
461 c1 k0 t) (CHead c3 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A
462 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
463 (\lambda (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C (CHead c1 k0 t)
464 (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
465 A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3
466 g (asucc g a) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3
467 g a c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1:
468 T).(eq C (CHead c1 k0 t) (CHead c3 (Bind Void) v1))))) (\lambda (b:
469 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
470 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
471 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))) (eq_ind_r K k
472 (\lambda (k1: K).(or3 (ex2 C (\lambda (c3: C).(eq C (CHead c1 k1 w) (CHead c3
473 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_:
474 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3:
475 C).(\lambda (v0: T).(\lambda (_: A).(eq C (CHead c1 k1 w) (CHead c3 (Bind
476 Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3
477 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a)
478 c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))
479 (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead
480 c1 k1 w) (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_:
481 C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b: B).(\lambda (_:
482 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
483 C).(\lambda (_: T).(csubc g c3 c2))))))) (let H9 \def (eq_ind C c0 (\lambda
484 (c: C).((eq C c (CHead c2 k w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1
485 (CHead c3 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_:
486 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3:
487 C).(\lambda (v0: T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v0)))))
488 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda
489 (c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0))))
490 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C
491 T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind
492 Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
493 b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void)))))
494 (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2)))))))) H2 c2
495 H8) in (let H10 \def (eq_ind C c0 (\lambda (c: C).(csubc g c1 c)) H1 c2 H8)
496 in (or3_intro0 (ex2 C (\lambda (c3: C).(eq C (CHead c1 k w) (CHead c3 k w)))
497 (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
498 T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0:
499 T).(\lambda (_: A).(eq C (CHead c1 k w) (CHead c3 (Bind Abst) v0)))))
500 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda
501 (c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0))))
502 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C
503 T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead c1 k w)
504 (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
505 T).(eq K k (Bind b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not
506 (eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g
507 c3 c2))))) (ex_intro2 C (\lambda (c3: C).(eq C (CHead c1 k w) (CHead c3 k
508 w))) (\lambda (c3: C).(csubc g c3 c2)) c1 (refl_equal C (CHead c1 k w))
509 H10)))) k0 H7) v H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda (c0:
510 C).(\lambda (H1: (csubc g c1 c0)).(\lambda (H2: (((eq C c0 (CHead c2 k w))
511 \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3:
512 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
513 (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v: T).(\lambda (_:
514 A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3: C).(\lambda (_:
515 T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v:
516 T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_: C).(\lambda (_:
517 T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda
518 (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b:
519 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
520 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
521 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))))).(\lambda (b:
522 B).(\lambda (H3: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
523 T).(\lambda (H4: (eq C (CHead c0 (Bind b) u2) (CHead c2 k w))).(let H5 \def
524 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
525 [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 (Bind b)
526 u2) (CHead c2 k w) H4) in ((let H6 \def (f_equal C K (\lambda (e: C).(match e
527 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow (Bind b) | (CHead
528 _ k0 _) \Rightarrow k0])) (CHead c0 (Bind b) u2) (CHead c2 k w) H4) in ((let
529 H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
530 with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c0
531 (Bind b) u2) (CHead c2 k w) H4) in (\lambda (H8: (eq K (Bind b) k)).(\lambda
532 (H9: (eq C c0 c2)).(let H10 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead
533 c2 k w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda
534 (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
535 T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
536 T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3:
537 C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
538 C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_:
539 C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda
540 (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void)
541 v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind
542 b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
543 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3
544 c2)))))))) H2 c2 H9) in (let H11 \def (eq_ind C c0 (\lambda (c: C).(csubc g
545 c1 c)) H1 c2 H9) in (let H12 \def (eq_ind_r K k (\lambda (k0: K).((eq C c2
546 (CHead c2 k0 w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k0 w)))
547 (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
548 T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
549 T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3:
550 C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
551 C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_:
552 C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda
553 (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void)
554 v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(eq K k0 (Bind
555 b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
556 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3
557 c2)))))))) H10 (Bind b) H8) in (eq_ind K (Bind b) (\lambda (k0: K).(or3 (ex2
558 C (\lambda (c3: C).(eq C (CHead c1 (Bind Void) u1) (CHead c3 k0 w))) (\lambda
559 (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
560 T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
561 T).(\lambda (_: A).(eq C (CHead c1 (Bind Void) u1) (CHead c3 (Bind Abst)
562 v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2))))
563 (\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v))))
564 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C
565 T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead c1 (Bind
566 Void) u1) (CHead c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda (_:
567 C).(\lambda (_: T).(eq K k0 (Bind b0))))) (\lambda (b0: B).(\lambda (_:
568 C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3:
569 C).(\lambda (_: T).(csubc g c3 c2))))))) (or3_intro2 (ex2 C (\lambda (c3:
570 C).(eq C (CHead c1 (Bind Void) u1) (CHead c3 (Bind b) w))) (\lambda (c3:
571 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
572 (_: A).(eq K (Bind b) (Bind Abbr))))) (\lambda (c3: C).(\lambda (v:
573 T).(\lambda (_: A).(eq C (CHead c1 (Bind Void) u1) (CHead c3 (Bind Abst)
574 v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2))))
575 (\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v))))
576 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C
577 T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead c1 (Bind
578 Void) u1) (CHead c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda (_:
579 C).(\lambda (_: T).(eq K (Bind b) (Bind b0))))) (\lambda (b0: B).(\lambda (_:
580 C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3:
581 C).(\lambda (_: T).(csubc g c3 c2))))) (ex4_3_intro B C T (\lambda (_:
582 B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead c1 (Bind Void) u1) (CHead
583 c3 (Bind Void) v1))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(eq K
584 (Bind b) (Bind b0))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not
585 (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g
586 c3 c2)))) b c1 u1 (refl_equal C (CHead c1 (Bind Void) u1)) (refl_equal K
587 (Bind b)) H3 H11)) k H8))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda
588 (c0: C).(\lambda (H1: (csubc g c1 c0)).(\lambda (H2: (((eq C c0 (CHead c2 k
589 w)) \to (or3 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3:
590 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
591 (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v: T).(\lambda (_:
592 A).(eq C c1 (CHead c3 (Bind Abst) v))))) (\lambda (c3: C).(\lambda (_:
593 T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v:
594 T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda (_: C).(\lambda (_:
595 T).(\lambda (a: A).(sc3 g a c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda
596 (c3: C).(\lambda (v1: T).(eq C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b:
597 B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b:
598 B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
599 B).(\lambda (c3: C).(\lambda (_: T).(csubc g c3 c2))))))))).(\lambda (v:
600 T).(\lambda (a: A).(\lambda (H3: (sc3 g (asucc g a) c1 v)).(\lambda (w0:
601 T).(\lambda (H4: (sc3 g a c0 w0)).(\lambda (H5: (eq C (CHead c0 (Bind Abbr)
602 w0) (CHead c2 k w))).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C
603 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _)
604 \Rightarrow c])) (CHead c0 (Bind Abbr) w0) (CHead c2 k w) H5) in ((let H7
605 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
606 with [(CSort _) \Rightarrow (Bind Abbr) | (CHead _ k0 _) \Rightarrow k0]))
607 (CHead c0 (Bind Abbr) w0) (CHead c2 k w) H5) in ((let H8 \def (f_equal C T
608 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
609 \Rightarrow w0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 (Bind Abbr) w0)
610 (CHead c2 k w) H5) in (\lambda (H9: (eq K (Bind Abbr) k)).(\lambda (H10: (eq
611 C c0 c2)).(let H11 \def (eq_ind T w0 (\lambda (t: T).(sc3 g a c0 t)) H4 w H8)
612 in (let H12 \def (eq_ind C c0 (\lambda (c: C).(sc3 g a c w)) H11 c2 H10) in
613 (let H13 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c2 k w)) \to (or3
614 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3: C).(csubc g
615 c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
616 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C c1
617 (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
618 A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3
619 g (asucc g a0) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
620 A).(sc3 g a0 c2 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda
621 (v1: T).(eq C c1 (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_:
622 C).(\lambda (_: T).(eq K k (Bind b))))) (\lambda (b: B).(\lambda (_:
623 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
624 C).(\lambda (_: T).(csubc g c3 c2)))))))) H2 c2 H10) in (let H14 \def (eq_ind
625 C c0 (\lambda (c: C).(csubc g c1 c)) H1 c2 H10) in (let H15 \def (eq_ind_r K
626 k (\lambda (k0: K).((eq C c2 (CHead c2 k0 w)) \to (or3 (ex2 C (\lambda (c3:
627 C).(eq C c1 (CHead c3 k0 w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A
628 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k0 (Bind Abbr)))))
629 (\lambda (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind
630 Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3
631 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0)
632 c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2
633 w))))) (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C
634 c1 (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
635 T).(eq K k0 (Bind b))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_: T).(not
636 (eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g
637 c3 c2)))))))) H13 (Bind Abbr) H9) in (eq_ind K (Bind Abbr) (\lambda (k0:
638 K).(or3 (ex2 C (\lambda (c3: C).(eq C (CHead c1 (Bind Abst) v) (CHead c3 k0
639 w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda
640 (_: T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda
641 (v0: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abst)
642 v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2))))
643 (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0) c3
644 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2 w)))))
645 (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead
646 c1 (Bind Abst) v) (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_:
647 C).(\lambda (_: T).(eq K k0 (Bind b))))) (\lambda (b: B).(\lambda (_:
648 C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
649 C).(\lambda (_: T).(csubc g c3 c2))))))) (or3_intro1 (ex2 C (\lambda (c3:
650 C).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abbr) w))) (\lambda (c3:
651 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
652 (_: A).(eq K (Bind Abbr) (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0:
653 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abst)
654 v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2))))
655 (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0) c3
656 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2 w)))))
657 (ex4_3 B C T (\lambda (_: B).(\lambda (c3: C).(\lambda (v1: T).(eq C (CHead
658 c1 (Bind Abst) v) (CHead c3 (Bind Void) v1))))) (\lambda (b: B).(\lambda (_:
659 C).(\lambda (_: T).(eq K (Bind Abbr) (Bind b))))) (\lambda (b: B).(\lambda
660 (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
661 C).(\lambda (_: T).(csubc g c3 c2))))) (ex5_3_intro C T A (\lambda (_:
662 C).(\lambda (_: T).(\lambda (_: A).(eq K (Bind Abbr) (Bind Abbr))))) (\lambda
663 (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) v)
664 (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
665 A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3
666 g (asucc g a0) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
667 A).(sc3 g a0 c2 w)))) c1 v a (refl_equal K (Bind Abbr)) (refl_equal C (CHead
668 c1 (Bind Abst) v)) H14 H3 H12)) k H9))))))))) H7)) H6)))))))))))) x y H0)))