1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/fwd".
19 include "csub3/defs.ma".
21 theorem csub3_gen_abbr:
22 \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csub3 g
23 (CHead e1 (Bind Abbr) v) c2) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2
24 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))))
26 \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda
27 (H: (csub3 g (CHead e1 (Bind Abbr) v) c2)).(let H0 \def (match H in csub3
28 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3 ? c c0)).((eq C c
29 (CHead e1 (Bind Abbr) v)) \to ((eq C c0 c2) \to (ex2 C (\lambda (e2: C).(eq C
30 c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))))) with
31 [(csub3_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead e1 (Bind
32 Abbr) v))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def (eq_ind C (CSort
33 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
34 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind Abbr)
35 v) H0) in (False_ind ((eq C (CSort n) c2) \to (ex2 C (\lambda (e2: C).(eq C
36 c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))) H2)) H1)))
37 | (csub3_head c1 c0 H0 k u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u)
38 (CHead e1 (Bind Abbr) v))).(\lambda (H2: (eq C (CHead c0 k u) c2)).((let H3
39 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
40 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u)
41 (CHead e1 (Bind Abbr) v) H1) in ((let H4 \def (f_equal C K (\lambda (e:
42 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
43 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind Abbr) v) H1)
44 in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
45 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c]))
46 (CHead c1 k u) (CHead e1 (Bind Abbr) v) H1) in (eq_ind C e1 (\lambda (c:
47 C).((eq K k (Bind Abbr)) \to ((eq T u v) \to ((eq C (CHead c0 k u) c2) \to
48 ((csub3 g c c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr)
49 v))) (\lambda (e2: C).(csub3 g e1 e2)))))))) (\lambda (H6: (eq K k (Bind
50 Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T u v) \to ((eq C (CHead
51 c0 k0 u) c2) \to ((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead
52 e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2))))))) (\lambda (H7: (eq
53 T u v)).(eq_ind T v (\lambda (t: T).((eq C (CHead c0 (Bind Abbr) t) c2) \to
54 ((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr)
55 v))) (\lambda (e2: C).(csub3 g e1 e2)))))) (\lambda (H8: (eq C (CHead c0
56 (Bind Abbr) v) c2)).(eq_ind C (CHead c0 (Bind Abbr) v) (\lambda (c:
57 C).((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind Abbr)
58 v))) (\lambda (e2: C).(csub3 g e1 e2))))) (\lambda (H9: (csub3 g e1 c0)).(let
59 H10 \def (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abbr) v) c))
60 H (CHead c0 (Bind Abbr) v) H8) in (ex_intro2 C (\lambda (e2: C).(eq C (CHead
61 c0 (Bind Abbr) v) (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1
62 e2)) c0 (refl_equal C (CHead c0 (Bind Abbr) v)) H9))) c2 H8)) u (sym_eq T u v
63 H7))) k (sym_eq K k (Bind Abbr) H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2
64 H0))) | (csub3_void c1 c0 H0 b H1 u1 u2) \Rightarrow (\lambda (H2: (eq C
65 (CHead c1 (Bind Void) u1) (CHead e1 (Bind Abbr) v))).(\lambda (H3: (eq C
66 (CHead c0 (Bind b) u2) c2)).((let H4 \def (eq_ind C (CHead c1 (Bind Void) u1)
67 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
68 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
69 (_: K).Prop) with [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_:
70 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void
71 \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abbr)
72 v) H2) in (False_ind ((eq C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c1 c0)
73 \to ((not (eq B b Void)) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind
74 Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))) H4)) H3 H0 H1))) |
75 (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind
76 Abst) t) (CHead e1 (Bind Abbr) v))).(\lambda (H3: (eq C (CHead c0 (Bind Abbr)
77 u) c2)).((let H4 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e:
78 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
79 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
80 with [(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with
81 [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) |
82 (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H2) in (False_ind
83 ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g c1 c0) \to ((ty3 g c0 u t)
84 \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2:
85 C).(csub3 g e1 e2)))))) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead e1
86 (Bind Abbr) v)) (refl_equal C c2))))))).
88 theorem csub3_gen_abst:
89 \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csub3 g
90 (CHead e1 (Bind Abst) v1) c2) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead
91 e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda
92 (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
93 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
96 \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v1: T).(\lambda
97 (H: (csub3 g (CHead e1 (Bind Abst) v1) c2)).(let H0 \def (match H in csub3
98 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3 ? c c0)).((eq C c
99 (CHead e1 (Bind Abst) v1)) \to ((eq C c0 c2) \to (or (ex2 C (\lambda (e2:
100 C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
101 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
102 v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
103 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))))) with [(csub3_sort n)
104 \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead e1 (Bind Abst)
105 v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def (eq_ind C (CSort n)
106 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
107 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind Abst)
108 v1) H0) in (False_ind ((eq C (CSort n) c2) \to (or (ex2 C (\lambda (e2:
109 C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
110 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
111 v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
112 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))) H2)) H1))) | (csub3_head c1 c0 H0 k
113 u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind Abst)
114 v1))).(\lambda (H2: (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T
115 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
116 \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind
117 Abst) v1) H1) in ((let H4 \def (f_equal C K (\lambda (e: C).(match e in C
118 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
119 \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind Abst) v1) H1) in ((let H5
120 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
121 with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k
122 u) (CHead e1 (Bind Abst) v1) H1) in (eq_ind C e1 (\lambda (c: C).((eq K k
123 (Bind Abst)) \to ((eq T u v1) \to ((eq C (CHead c0 k u) c2) \to ((csub3 g c
124 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
125 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
126 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
127 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
128 v1)))))))))) (\lambda (H6: (eq K k (Bind Abst))).(eq_ind K (Bind Abst)
129 (\lambda (k0: K).((eq T u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csub3 g e1
130 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
131 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
132 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
133 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
134 v1))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
135 (CHead c0 (Bind Abst) t) c2) \to ((csub3 g e1 c0) \to (or (ex2 C (\lambda
136 (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1
137 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
138 Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
139 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) (\lambda (H8: (eq C (CHead c0
140 (Bind Abst) v1) c2)).(eq_ind C (CHead c0 (Bind Abst) v1) (\lambda (c:
141 C).((csub3 g e1 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind
142 Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2:
143 C).(\lambda (v2: T).(eq C c (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
144 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
145 e2 v2 v1))))))) (\lambda (H9: (csub3 g e1 c0)).(let H10 \def (eq_ind_r C c2
146 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abst) v1) c)) H (CHead c0 (Bind
147 Abst) v1) H8) in (or_introl (ex2 C (\lambda (e2: C).(eq C (CHead c0 (Bind
148 Abst) v1) (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
149 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c0 (Bind Abst) v1)
150 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1
151 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))) (ex_intro2 C
152 (\lambda (e2: C).(eq C (CHead c0 (Bind Abst) v1) (CHead e2 (Bind Abst) v1)))
153 (\lambda (e2: C).(csub3 g e1 e2)) c0 (refl_equal C (CHead c0 (Bind Abst) v1))
154 H9)))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind Abst) H6))) c1
155 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csub3_void c1 c0 H0 b H1 u1 u2)
156 \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind
157 Abst) v1))).(\lambda (H3: (eq C (CHead c0 (Bind b) u2) c2)).((let H4 \def
158 (eq_ind C (CHead c1 (Bind Void) u1) (\lambda (e: C).(match e in C return
159 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
160 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b0)
161 \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
162 \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat
163 _) \Rightarrow False])])) I (CHead e1 (Bind Abst) v1) H2) in (False_ind ((eq
164 C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c1 c0) \to ((not (eq B b Void))
165 \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda
166 (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
167 c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1
168 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) H4)) H3 H0
169 H1))) | (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C (CHead
170 c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1))).(\lambda (H3: (eq C (CHead c0
171 (Bind Abbr) u) c2)).((let H4 \def (f_equal C T (\lambda (e: C).(match e in C
172 return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0)
173 \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1) H2) in
174 ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
175 C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead
176 c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1) H2) in (eq_ind C e1 (\lambda (c:
177 C).((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g c c0)
178 \to ((ty3 g c0 u t) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind
179 Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2:
180 C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
181 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
182 e2 v2 v1)))))))))) (\lambda (H6: (eq T t v1)).(eq_ind T v1 (\lambda (t0:
183 T).((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g c0 u
184 t0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
185 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
186 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
187 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
188 v1))))))))) (\lambda (H7: (eq C (CHead c0 (Bind Abbr) u) c2)).(eq_ind C
189 (CHead c0 (Bind Abbr) u) (\lambda (c: C).((csub3 g e1 c0) \to ((ty3 g c0 u
190 v1) \to (or (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind Abst) v1)))
191 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
192 T).(eq C c (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
193 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
194 v1)))))))) (\lambda (H8: (csub3 g e1 c0)).(\lambda (H9: (ty3 g c0 u v1)).(let
195 H10 \def (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abst) v1)
196 c)) H (CHead c0 (Bind Abbr) u) H7) in (or_intror (ex2 C (\lambda (e2: C).(eq
197 C (CHead c0 (Bind Abbr) u) (CHead e2 (Bind Abst) v1))) (\lambda (e2:
198 C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
199 (CHead c0 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
200 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
201 e2 v2 v1)))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead
202 c0 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
203 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1))) c0
204 u (refl_equal C (CHead c0 (Bind Abbr) u)) H8 H9))))) c2 H7)) t (sym_eq T t v1
205 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead
206 e1 (Bind Abst) v1)) (refl_equal C c2))))))).
208 theorem csub3_gen_bind:
209 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
210 (v1: T).((csub3 g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
211 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
212 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))))
214 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
215 (v1: T).(\lambda (H: (csub3 g (CHead e1 (Bind b1) v1) c2)).(let H0 \def
216 (match H in csub3 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3
217 ? c c0)).((eq C c (CHead e1 (Bind b1) v1)) \to ((eq C c0 c2) \to (ex2_3 B C T
218 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
219 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
220 e2)))))))))) with [(csub3_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n)
221 (CHead e1 (Bind b1) v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def
222 (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
223 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
224 False])) I (CHead e1 (Bind b1) v1) H0) in (False_ind ((eq C (CSort n) c2) \to
225 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
226 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
227 T).(csub3 g e1 e2)))))) H2)) H1))) | (csub3_head c1 c0 H0 k u) \Rightarrow
228 (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(\lambda (H2:
229 (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T (\lambda (e: C).(match e
230 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
231 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in ((let H4 \def
232 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
233 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u)
234 (CHead e1 (Bind b1) v1) H1) in ((let H5 \def (f_equal C C (\lambda (e:
235 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 |
236 (CHead c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in
237 (eq_ind C e1 (\lambda (c: C).((eq K k (Bind b1)) \to ((eq T u v1) \to ((eq C
238 (CHead c0 k u) c2) \to ((csub3 g c c0) \to (ex2_3 B C T (\lambda (b2:
239 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
240 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))))
241 (\lambda (H6: (eq K k (Bind b1))).(eq_ind K (Bind b1) (\lambda (k0: K).((eq T
242 u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csub3 g e1 c0) \to (ex2_3 B C T
243 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
244 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
245 e2))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
246 (CHead c0 (Bind b1) t) c2) \to ((csub3 g e1 c0) \to (ex2_3 B C T (\lambda
247 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2)
248 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
249 e2)))))))) (\lambda (H8: (eq C (CHead c0 (Bind b1) v1) c2)).(eq_ind C (CHead
250 c0 (Bind b1) v1) (\lambda (c: C).((csub3 g e1 c0) \to (ex2_3 B C T (\lambda
251 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
252 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))
253 (\lambda (H9: (csub3 g e1 c0)).(let H10 \def (eq_ind_r C c2 (\lambda (c:
254 C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b1) v1) H8) in
255 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
256 (CHead c0 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
257 (e2: C).(\lambda (_: T).(csub3 g e1 e2)))) b1 c0 v1 (refl_equal C (CHead c0
258 (Bind b1) v1)) H9))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind b1)
259 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csub3_void c1 c0 H0 b H1
260 u1 u2) \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind Void) u1) (CHead e1
261 (Bind b1) v1))).(\lambda (H3: (eq C (CHead c0 (Bind b) u2) c2)).((let H4 \def
262 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
263 [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c1 (Bind
264 Void) u1) (CHead e1 (Bind b1) v1) H2) in ((let H5 \def (f_equal C B (\lambda
265 (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
266 Void | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
267 [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Void])])) (CHead c1 (Bind
268 Void) u1) (CHead e1 (Bind b1) v1) H2) in ((let H6 \def (f_equal C C (\lambda
269 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1
270 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind Void) u1) (CHead e1 (Bind
271 b1) v1) H2) in (eq_ind C e1 (\lambda (c: C).((eq B Void b1) \to ((eq T u1 v1)
272 \to ((eq C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c c0) \to ((not (eq B b
273 Void)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
274 T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
275 C).(\lambda (_: T).(csub3 g e1 e2))))))))))) (\lambda (H7: (eq B Void
276 b1)).(eq_ind B Void (\lambda (_: B).((eq T u1 v1) \to ((eq C (CHead c0 (Bind
277 b) u2) c2) \to ((csub3 g e1 c0) \to ((not (eq B b Void)) \to (ex2_3 B C T
278 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
279 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
280 e2)))))))))) (\lambda (H8: (eq T u1 v1)).(eq_ind T v1 (\lambda (_: T).((eq C
281 (CHead c0 (Bind b) u2) c2) \to ((csub3 g e1 c0) \to ((not (eq B b Void)) \to
282 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
283 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
284 T).(csub3 g e1 e2))))))))) (\lambda (H9: (eq C (CHead c0 (Bind b) u2)
285 c2)).(eq_ind C (CHead c0 (Bind b) u2) (\lambda (c: C).((csub3 g e1 c0) \to
286 ((not (eq B b Void)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
287 C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_:
288 B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))) (\lambda (H10:
289 (csub3 g e1 c0)).(\lambda (_: (not (eq B b Void))).(let H12 \def (eq_ind_r C
290 c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b)
291 u2) H9) in (let H13 \def (eq_ind_r B b1 (\lambda (b0: B).(csub3 g (CHead e1
292 (Bind b0) v1) (CHead c0 (Bind b) u2))) H12 Void H7) in (ex2_3_intro B C T
293 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c0 (Bind b)
294 u2) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
295 T).(csub3 g e1 e2)))) b c0 u2 (refl_equal C (CHead c0 (Bind b) u2)) H10)))))
296 c2 H9)) u1 (sym_eq T u1 v1 H8))) b1 H7)) c1 (sym_eq C c1 e1 H6))) H5)) H4))
297 H3 H0 H1))) | (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C
298 (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1))).(\lambda (H3: (eq C (CHead
299 c0 (Bind Abbr) u) c2)).((let H4 \def (f_equal C T (\lambda (e: C).(match e in
300 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0)
301 \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in
302 ((let H5 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
303 C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
304 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
305 \Rightarrow Abst])])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in
306 ((let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
307 C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead
308 c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in (eq_ind C e1 (\lambda (c:
309 C).((eq B Abst b1) \to ((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2)
310 \to ((csub3 g c c0) \to ((ty3 g c0 u t) \to (ex2_3 B C T (\lambda (b2:
311 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
312 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))))))
313 (\lambda (H7: (eq B Abst b1)).(eq_ind B Abst (\lambda (_: B).((eq T t v1) \to
314 ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g c0 u t)
315 \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
316 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
317 T).(csub3 g e1 e2)))))))))) (\lambda (H8: (eq T t v1)).(eq_ind T v1 (\lambda
318 (t0: T).((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g
319 c0 u t0) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
320 T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
321 C).(\lambda (_: T).(csub3 g e1 e2))))))))) (\lambda (H9: (eq C (CHead c0
322 (Bind Abbr) u) c2)).(eq_ind C (CHead c0 (Bind Abbr) u) (\lambda (c:
323 C).((csub3 g e1 c0) \to ((ty3 g c0 u v1) \to (ex2_3 B C T (\lambda (b2:
324 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
325 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))
326 (\lambda (H10: (csub3 g e1 c0)).(\lambda (_: (ty3 g c0 u v1)).(let H12 \def
327 (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead
328 c0 (Bind Abbr) u) H9) in (let H13 \def (eq_ind_r B b1 (\lambda (b: B).(csub3
329 g (CHead e1 (Bind b) v1) (CHead c0 (Bind Abbr) u))) H12 Abst H7) in
330 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
331 (CHead c0 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
332 (e2: C).(\lambda (_: T).(csub3 g e1 e2)))) Abbr c0 u (refl_equal C (CHead c0
333 (Bind Abbr) u)) H10))))) c2 H9)) t (sym_eq T t v1 H8))) b1 H7)) c1 (sym_eq C
334 c1 e1 H6))) H5)) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead e1 (Bind b1)
335 v1)) (refl_equal C c2)))))))).