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