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/csuba/defs.ma".
19 theorem csuba_gen_abbr:
20 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
21 (CHead d1 (Bind Abbr) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
22 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
24 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
25 (csuba g (CHead d1 (Bind Abbr) u) c)).(insert_eq C (CHead d1 (Bind Abbr) u)
26 (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
27 C c (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (\lambda
28 (y: C).(\lambda (H0: (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda
29 (c1: C).((eq C c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(eq C
30 c1 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda
31 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abbr) u))).(let H2
32 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
33 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
34 False])) I (CHead d1 (Bind Abbr) u) H1) in (False_ind (ex2 C (\lambda (d2:
35 C).(eq C (CSort n) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
36 d2))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
37 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
38 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
39 d2)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c1 k u0)
40 (CHead d1 (Bind Abbr) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
41 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
42 _) \Rightarrow c0])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H3) in ((let H5
43 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
44 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
45 u0) (CHead d1 (Bind Abbr) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
46 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
47 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H3)
48 in (\lambda (H7: (eq K k (Bind Abbr))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r
49 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k t) (CHead d2
50 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (eq_ind_r K (Bind Abbr)
51 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u) (CHead d2
52 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H9 \def (eq_ind C
53 c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
54 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
55 d2))))) H2 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0
56 c2)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr)
57 u) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) c2
58 (refl_equal C (CHead c2 (Bind Abbr) u)) H10))) k H7) u0 H6)))) H5))
59 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
60 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
61 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
62 d2)))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
63 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u1) (CHead d1
64 (Bind Abbr) u))).(let H5 \def (eq_ind C (CHead c1 (Bind Void) u1) (\lambda
65 (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
66 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
67 (_: K).Prop) with [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_:
68 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void
69 \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead d1 (Bind Abbr)
70 u) H4) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind b) u2)
71 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) H5)))))))))))
72 (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_:
73 (((eq C c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(eq C c2
74 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))).(\lambda (t:
75 T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g a))).(\lambda (u0:
76 T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst)
77 t) (CHead d1 (Bind Abbr) u))).(let H6 \def (eq_ind C (CHead c1 (Bind Abst) t)
78 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
79 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
80 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
81 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void
82 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1 (Bind Abbr)
83 u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u0)
84 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) H6))))))))))))
90 theorem csuba_gen_void:
91 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
92 (CHead d1 (Bind Void) u1) c) \to (ex2_3 B C T (\lambda (b: B).(\lambda (d2:
93 C).(\lambda (u2: T).(eq C c (CHead d2 (Bind b) u2))))) (\lambda (_:
94 B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))))))
96 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
97 (H: (csuba g (CHead d1 (Bind Void) u1) c)).(insert_eq C (CHead d1 (Bind Void)
98 u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2_3 B C T (\lambda
99 (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Bind b) u2)))))
100 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))))
101 (\lambda (y: C).(\lambda (H0: (csuba g y c)).(csuba_ind g (\lambda (c0:
102 C).(\lambda (c1: C).((eq C c0 (CHead d1 (Bind Void) u1)) \to (ex2_3 B C T
103 (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Bind b)
104 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
105 d2)))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind
106 Void) u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C
107 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
108 \Rightarrow False])) I (CHead d1 (Bind Void) u1) H1) in (False_ind (ex2_3 B C
109 T (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2
110 (Bind b) u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
111 d2))))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
112 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Void) u1)) \to (ex2_3 B C T
113 (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Bind b)
114 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
115 d2)))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
116 (CHead d1 (Bind Void) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match
117 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
118 _) \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Bind Void) u1) H3) in ((let H5
119 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
120 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
121 u) (CHead d1 (Bind Void) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
122 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
123 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead d1 (Bind Void) u1) H3)
124 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r
125 T u1 (\lambda (t: T).(ex2_3 B C T (\lambda (b: B).(\lambda (d2: C).(\lambda
126 (u2: T).(eq C (CHead c2 k t) (CHead d2 (Bind b) u2))))) (\lambda (_:
127 B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))) (eq_ind_r K (Bind
128 Void) (\lambda (k0: K).(ex2_3 B C T (\lambda (b: B).(\lambda (d2: C).(\lambda
129 (u2: T).(eq C (CHead c2 k0 u1) (CHead d2 (Bind b) u2))))) (\lambda (_:
130 B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))) (let H9 \def (eq_ind
131 C c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u1)) \to (ex2_3 B C T
132 (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Bind b)
133 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
134 d2))))))) H2 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g
135 c0 c2)) H1 d1 H8) in (ex2_3_intro B C T (\lambda (b: B).(\lambda (d2:
136 C).(\lambda (u2: T).(eq C (CHead c2 (Bind Void) u1) (CHead d2 (Bind b)
137 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))
138 Void c2 u1 (refl_equal C (CHead c2 (Bind Void) u1)) H10))) k H7) u H6))))
139 H5)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
140 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Void) u1)) \to (ex2_3 B C T
141 (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Bind b)
142 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
143 d2)))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u0:
144 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u0) (CHead d1
145 (Bind Void) u1))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C
146 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _)
147 \Rightarrow c0])) (CHead c1 (Bind Void) u0) (CHead d1 (Bind Void) u1) H4) in
148 ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
149 C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead
150 c1 (Bind Void) u0) (CHead d1 (Bind Void) u1) H4) in (\lambda (H7: (eq C c1
151 d1)).(let H8 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind
152 Void) u1)) \to (ex2_3 B C T (\lambda (b0: B).(\lambda (d2: C).(\lambda (u3:
153 T).(eq C c2 (CHead d2 (Bind b0) u3))))) (\lambda (_: B).(\lambda (d2:
154 C).(\lambda (_: T).(csuba g d1 d2))))))) H2 d1 H7) in (let H9 \def (eq_ind C
155 c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1 H7) in (ex2_3_intro B C T (\lambda
156 (b0: B).(\lambda (d2: C).(\lambda (u3: T).(eq C (CHead c2 (Bind b) u2) (CHead
157 d2 (Bind b0) u3))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba
158 g d1 d2)))) b c2 u2 (refl_equal C (CHead c2 (Bind b) u2)) H9)))))
159 H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
160 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Void) u1)) \to (ex2_3 B C T
161 (\lambda (b: B).(\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Bind b)
162 u2))))) (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1
163 d2)))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc
164 g a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
165 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Void) u1))).(let H6 \def (eq_ind C
166 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
167 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
168 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
169 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
170 True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
171 (Bind Void) u1) H5) in (False_ind (ex2_3 B C T (\lambda (b: B).(\lambda (d2:
172 C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind b) u2)))))
173 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))
174 H6)))))))))))) y c H0))) H))))).
179 theorem csuba_gen_abst:
180 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
181 (CHead d1 (Bind Abst) u1) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead
182 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
183 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
184 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
185 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
186 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
189 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
190 (H: (csuba g (CHead d1 (Bind Abst) u1) c)).(insert_eq C (CHead d1 (Bind Abst)
191 u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
192 C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
193 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
194 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
195 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
196 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
197 A).(arity g d2 u2 a))))))) (\lambda (y: C).(\lambda (H0: (csuba g y
198 c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0 (CHead d1 (Bind
199 Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst)
200 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
201 C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abbr) u2)))))
202 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
203 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
204 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))
205 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst)
206 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
207 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
208 \Rightarrow False])) I (CHead d1 (Bind Abst) u1) H1) in (False_ind (or (ex2 C
209 (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
210 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
211 (_: A).(eq C (CSort n) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
212 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
213 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
214 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) H2))))
215 (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda
216 (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2:
217 C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
218 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
219 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
220 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
221 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
222 A).(arity g d2 u2 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3:
223 (eq C (CHead c1 k u) (CHead d1 (Bind Abst) u1))).(let H4 \def (f_equal C C
224 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
225 \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 k u) (CHead d1
226 (Bind Abst) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in
227 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
228 \Rightarrow k0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H3) in ((let H6
229 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
230 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u)
231 (CHead d1 (Bind Abst) u1) H3) in (\lambda (H7: (eq K k (Bind Abst))).(\lambda
232 (H8: (eq C c1 d1)).(eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2:
233 C).(eq C (CHead c2 k t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
234 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
235 (CHead c2 k t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
236 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
237 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
238 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (eq_ind_r K (Bind Abst)
239 (\lambda (k0: K).(or (ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u1) (CHead d2
240 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
241 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 k0 u1) (CHead d2
242 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
243 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
244 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
245 u2 a))))))) (let H9 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
246 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
247 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
248 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
249 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
250 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
251 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))) H2
252 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1
253 H8) in (or_introl (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1)
254 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
255 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst)
256 u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
257 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
258 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
259 (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2
260 (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
261 c2 (refl_equal C (CHead c2 (Bind Abst) u1)) H10)))) k H7) u H6)))) H5))
262 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
263 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C
264 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
265 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
266 C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
267 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
268 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
269 (a: A).(arity g d2 u2 a))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b
270 Void))).(\lambda (u0: T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1 (Bind
271 Void) u0) (CHead d1 (Bind Abst) u1))).(let H5 \def (eq_ind C (CHead c1 (Bind
272 Void) u0) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with
273 [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return
274 (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow (match b0 in B return
275 (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False |
276 Void \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead d1 (Bind
277 Abst) u1) H4) in (False_ind (or (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind
278 b) u2) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3
279 C T A (\lambda (d2: C).(\lambda (u3: T).(\lambda (_: A).(eq C (CHead c2 (Bind
280 b) u2) (CHead d2 (Bind Abbr) u3))))) (\lambda (d2: C).(\lambda (_:
281 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
282 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
283 (u3: T).(\lambda (a: A).(arity g d2 u3 a)))))) H5))))))))))) (\lambda (c1:
284 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c1
285 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
286 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
287 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr)
288 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
289 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
290 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
291 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc
292 g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u a)).(\lambda (H5: (eq C
293 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1))).(let H6 \def (f_equal C
294 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
295 \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind Abst) t)
296 (CHead d1 (Bind Abst) u1) H5) in ((let H7 \def (f_equal C T (\lambda (e:
297 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t |
298 (CHead _ _ t0) \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead d1 (Bind
299 Abst) u1) H5) in (\lambda (H8: (eq C c1 d1)).(let H9 \def (eq_ind T t
300 (\lambda (t0: T).(arity g c1 t0 (asucc g a))) H3 u1 H7) in (let H10 \def
301 (eq_ind C c1 (\lambda (c0: C).(arity g c0 u1 (asucc g a))) H9 d1 H8) in (let
302 H11 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abst) u1))
303 \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda
304 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
305 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
306 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
307 C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0))))) (\lambda
308 (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0)))))))) H2 d1 H8)
309 in (let H12 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1 H8) in
310 (or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
311 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
312 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u)
313 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
314 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
315 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
316 A).(arity g d2 u2 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2:
317 T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr)
318 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
319 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g
320 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
321 a0)))) c2 u a (refl_equal C (CHead c2 (Bind Abbr) u)) H12 H10 H4))))))))
322 H6)))))))))))) y c H0))) H))))).
327 theorem csuba_gen_flat:
328 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
329 (f: F).((csuba g (CHead d1 (Flat f) u1) c) \to (ex2_2 C T (\lambda (d2:
330 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
331 C).(\lambda (_: T).(csuba g d1 d2)))))))))
333 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
334 (f: F).(\lambda (H: (csuba g (CHead d1 (Flat f) u1) c)).(insert_eq C (CHead
335 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2_2 C T
336 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
337 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (\lambda (y: C).(\lambda (H0:
338 (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0
339 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
340 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
341 d2))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
342 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
343 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
344 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
345 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
346 (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))) H2)))) (\lambda (c1:
347 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c1
348 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
349 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
350 d2))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
351 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
352 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
353 _) \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
354 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
355 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
356 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
357 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
358 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in
359 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r T u1
360 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2
361 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
362 d2))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
363 C).(\lambda (u2: T).(eq C (CHead c2 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
364 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (let H9 \def (eq_ind C c1
365 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
366 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
367 C).(\lambda (_: T).(csuba g d1 d2)))))) H2 d1 H8) in (let H10 \def (eq_ind C
368 c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1 H8) in (ex2_2_intro C T (\lambda
369 (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Flat f) u1) (CHead d2 (Flat f)
370 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))) c2 u1 (refl_equal C
371 (CHead c2 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
372 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c1
373 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
374 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
375 d2))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u0:
376 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u0) (CHead d1
377 (Flat f) u1))).(let H5 \def (eq_ind C (CHead c1 (Bind Void) u0) (\lambda (ee:
378 C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
379 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
380 with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1
381 (Flat f) u1) H4) in (False_ind (ex2_2 C T (\lambda (d2: C).(\lambda (u3:
382 T).(eq C (CHead c2 (Bind b) u2) (CHead d2 (Flat f) u3)))) (\lambda (d2:
383 C).(\lambda (_: T).(csuba g d1 d2)))) H5))))))))))) (\lambda (c1: C).(\lambda
384 (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Flat
385 f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2
386 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
387 d2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
388 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
389 (CHead c1 (Bind Abst) t) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
390 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
391 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
392 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
393 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
394 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
395 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))
396 H6)))))))))))) y c H0))) H)))))).
401 theorem csuba_gen_bind:
402 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
403 (v1: T).((csuba g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
404 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
405 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
407 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
408 (v1: T).(\lambda (H: (csuba g (CHead e1 (Bind b1) v1) c2)).(insert_eq C
409 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c c2)) (\lambda (_:
410 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
411 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
412 T).(csuba g e1 e2)))))) (\lambda (y: C).(\lambda (H0: (csuba g y
413 c2)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind
414 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
415 T).(eq C c0 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
416 C).(\lambda (_: T).(csuba g e1 e2)))))))) (\lambda (n: nat).(\lambda (H1: (eq
417 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
418 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
419 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
420 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
421 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
422 (e2: C).(\lambda (_: T).(csuba g e1 e2))))) H2)))) (\lambda (c1: C).(\lambda
423 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1
424 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
425 (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
426 C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (k: K).(\lambda (u:
427 T).(\lambda (H3: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
428 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
429 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k u)
430 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
431 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
432 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H3)
433 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
434 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
435 (CHead c1 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
436 b1))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
437 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k t)
438 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
439 T).(csuba g e1 e2)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
440 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k0 v1)
441 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
442 T).(csuba g e1 e2)))))) (let H9 \def (eq_ind C c1 (\lambda (c: C).((eq C c
443 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
444 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
445 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H2 e1 H8) in (let
446 H10 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c3)) H1 e1 H8) in
447 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
448 (CHead c3 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
449 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) b1 c3 v1 (refl_equal C (CHead c3
450 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
451 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1
452 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
453 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
454 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (b:
455 B).(\lambda (_: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
456 T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1)
457 v1))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
458 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c]))
459 (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1) v1) H4) in ((let H6 \def
460 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
461 [(CSort _) \Rightarrow Void | (CHead _ k _) \Rightarrow (match k in K return
462 (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
463 Void])])) (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1) v1) H4) in ((let H7
464 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
465 with [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c1
466 (Bind Void) u1) (CHead e1 (Bind b1) v1) H4) in (\lambda (H8: (eq B Void
467 b1)).(\lambda (H9: (eq C c1 e1)).(let H10 \def (eq_ind C c1 (\lambda (c:
468 C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
469 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2)))))
470 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H2 e1
471 H9) in (let H11 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c3)) H1 e1 H9)
472 in (let H12 \def (eq_ind_r B b1 (\lambda (b0: B).((eq C e1 (CHead e1 (Bind
473 b0) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
474 T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
475 C).(\lambda (_: T).(csuba g e1 e2))))))) H10 Void H8) in (ex2_3_intro B C T
476 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind b)
477 u2) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
478 T).(csuba g e1 e2)))) b c3 u2 (refl_equal C (CHead c3 (Bind b) u2))
479 H11))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H1:
480 (csuba g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1 (Bind b1) v1)) \to (ex2_3
481 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2
482 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
483 e1 e2)))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H3: (arity g c1 t
484 (asucc g a))).(\lambda (u: T).(\lambda (_: (arity g c3 u a)).(\lambda (H5:
485 (eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1))).(let H6 \def
486 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
487 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind
488 Abst) t) (CHead e1 (Bind b1) v1) H5) in ((let H7 \def (f_equal C B (\lambda
489 (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
490 Abst | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
491 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead c1 (Bind
492 Abst) t) (CHead e1 (Bind b1) v1) H5) in ((let H8 \def (f_equal C T (\lambda
493 (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t
494 | (CHead _ _ t0) \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind
495 b1) v1) H5) in (\lambda (H9: (eq B Abst b1)).(\lambda (H10: (eq C c1
496 e1)).(let H11 \def (eq_ind T t (\lambda (t0: T).(arity g c1 t0 (asucc g a)))
497 H3 v1 H8) in (let H12 \def (eq_ind C c1 (\lambda (c: C).(arity g c v1 (asucc
498 g a))) H11 e1 H10) in (let H13 \def (eq_ind C c1 (\lambda (c: C).((eq C c
499 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
500 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
501 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H2 e1 H10) in (let
502 H14 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c3)) H1 e1 H10) in (let H15
503 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1 (CHead e1 (Bind b) v1)) \to
504 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3
505 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
506 T).(csuba g e1 e2))))))) H13 Abst H9) in (ex2_3_intro B C T (\lambda (b2:
507 B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind Abbr) u) (CHead e2
508 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
509 e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H14))))))))) H7))
510 H6)))))))))))) y c2 H0))) H)))))).
515 theorem csuba_gen_abst_rev:
516 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
517 (CHead d1 (Bind Abst) u)) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
518 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
519 C).(\lambda (u2: T).(eq C c (CHead d2 (Bind Void) u2)))) (\lambda (d2:
520 C).(\lambda (_: T).(csuba g d2 d1)))))))))
522 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
523 (csuba g c (CHead d1 (Bind Abst) u))).(insert_eq C (CHead d1 (Bind Abst) u)
524 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
525 C).(eq C c (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
526 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Bind Void)
527 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (\lambda (y:
528 C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1:
529 C).((eq C c1 (CHead d1 (Bind Abst) u)) \to (or (ex2 C (\lambda (d2: C).(eq C
530 c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
531 (\lambda (d2: C).(\lambda (u2: T).(eq C c0 (CHead d2 (Bind Void) u2))))
532 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))) (\lambda (n:
533 nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst) u))).(let H2 \def
534 (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
535 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
536 False])) I (CHead d1 (Bind Abst) u) H1) in (False_ind (or (ex2 C (\lambda
537 (d2: C).(eq C (CSort n) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
538 d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead
539 d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))
540 H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
541 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (or (ex2 C
542 (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba
543 g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2
544 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
545 d1)))))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k
546 u0) (CHead d1 (Bind Abst) u))).(let H4 \def (f_equal C C (\lambda (e:
547 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 |
548 (CHead c0 _ _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3)
549 in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
550 (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
551 (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3) in ((let H6 \def (f_equal C T
552 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
553 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1
554 (Bind Abst) u) H3) in (\lambda (H7: (eq K k (Bind Abst))).(\lambda (H8: (eq C
555 c2 d1)).(eq_ind_r T u (\lambda (t: T).(or (ex2 C (\lambda (d2: C).(eq C
556 (CHead c1 k t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
557 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 k t) (CHead d2
558 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))
559 (eq_ind_r K (Bind Abst) (\lambda (k0: K).(or (ex2 C (\lambda (d2: C).(eq C
560 (CHead c1 k0 u) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
561 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 k0 u) (CHead d2
562 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (let
563 H9 \def (eq_ind C c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abst) u)) \to
564 (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2:
565 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1
566 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
567 d1))))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g
568 c1 c0)) H1 d1 H8) in (or_introl (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind
569 Abst) u) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
570 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) u) (CHead
571 d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
572 (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) u) (CHead d2 (Bind
573 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1 (Bind
574 Abst) u)) H10)))) k H7) u0 H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda
575 (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2 (CHead d1
576 (Bind Abst) u)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind
577 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
578 C).(\lambda (u2: T).(eq C c1 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
579 C).(\lambda (_: T).(csuba g d2 d1)))))))).(\lambda (b: B).(\lambda (H3: (not
580 (eq B b Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead
581 c2 (Bind b) u2) (CHead d1 (Bind Abst) u))).(let H5 \def (f_equal C C (\lambda
582 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2
583 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind b) u2) (CHead d1 (Bind
584 Abst) u) H4) in ((let H6 \def (f_equal C B (\lambda (e: C).(match e in C
585 return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _)
586 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0)
587 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead d1
588 (Bind Abst) u) H4) in ((let H7 \def (f_equal C T (\lambda (e: C).(match e in
589 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 | (CHead _ _ t)
590 \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead d1 (Bind Abst) u) H4) in
591 (\lambda (H8: (eq B b Abst)).(\lambda (H9: (eq C c2 d1)).(let H10 \def
592 (eq_ind B b (\lambda (b0: B).(not (eq B b0 Void))) H3 Abst H8) in (let H11
593 \def (eq_ind C c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abst) u)) \to
594 (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2:
595 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u3: T).(eq C c1
596 (CHead d2 (Bind Void) u3)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
597 d1))))))) H2 d1 H9) in (let H12 \def (eq_ind C c2 (\lambda (c0: C).(csuba g
598 c1 c0)) H1 d1 H9) in (or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind
599 Void) u1) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
600 (ex2_2 C T (\lambda (d2: C).(\lambda (u3: T).(eq C (CHead c1 (Bind Void) u1)
601 (CHead d2 (Bind Void) u3)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
602 d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u3: T).(eq C (CHead c1
603 (Bind Void) u1) (CHead d2 (Bind Void) u3)))) (\lambda (d2: C).(\lambda (_:
604 T).(csuba g d2 d1))) c1 u1 (refl_equal C (CHead c1 (Bind Void) u1))
605 H12)))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
606 (csuba g c1 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (or
607 (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2:
608 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1
609 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
610 d1)))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc
611 g a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
612 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Abst) u))).(let H6 \def (eq_ind C
613 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
614 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
615 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
616 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
617 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
618 d1 (Bind Abst) u) H5) in (False_ind (or (ex2 C (\lambda (d2: C).(eq C (CHead
619 c1 (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
620 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind
621 Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
622 g d2 d1))))) H6)))))))))))) c y H0))) H))))).
627 theorem csuba_gen_void_rev:
628 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
629 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
630 Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
632 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
633 (csuba g c (CHead d1 (Bind Void) u))).(insert_eq C (CHead d1 (Bind Void) u)
634 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
635 C c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (\lambda
636 (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda
637 (c1: C).((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
638 c0 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda
639 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H2
640 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
641 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
642 False])) I (CHead d1 (Bind Void) u) H1) in (False_ind (ex2 C (\lambda (d2:
643 C).(eq C (CSort n) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
644 d1))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
645 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
646 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
647 d1)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k u0)
648 (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
649 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
650 _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3) in ((let H5
651 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
652 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
653 u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
654 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
655 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3)
656 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
657 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead d2
658 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (eq_ind_r K (Bind Void)
659 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k0 u) (CHead d2
660 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H9 \def (eq_ind C
661 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
662 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
663 d1))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
664 c0)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void)
665 u) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)) c1
666 (refl_equal C (CHead c1 (Bind Void) u)) H10))) k H7) u0 H6)))) H5))
667 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
668 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
669 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
670 d1)))))).(\lambda (b: B).(\lambda (H3: (not (eq B b Void))).(\lambda (u1:
671 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CHead d1
672 (Bind Void) u))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C
673 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _)
674 \Rightarrow c0])) (CHead c2 (Bind b) u2) (CHead d1 (Bind Void) u) H4) in
675 ((let H6 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
676 C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K
677 return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
678 \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead d1 (Bind Void) u) H4) in
679 ((let H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
680 C).T) with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead
681 c2 (Bind b) u2) (CHead d1 (Bind Void) u) H4) in (\lambda (H8: (eq B b
682 Void)).(\lambda (H9: (eq C c2 d1)).(let H10 \def (eq_ind B b (\lambda (b0:
683 B).(not (eq B b0 Void))) H3 Void H8) in (let H11 \def (eq_ind C c2 (\lambda
684 (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
685 c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1))))) H2 d1 H9)
686 in (let H12 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H9) in
687 (let H13 \def (match (H10 (refl_equal B Void)) in False return (\lambda (_:
688 False).(ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void) u1) (CHead d2
689 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) with []) in H13)))))))
690 H6)) H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
691 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
692 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
693 d1)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
694 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
695 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Void) u))).(let H6 \def (eq_ind C
696 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
697 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
698 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
699 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
700 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
701 d1 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
702 (Bind Abst) t) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))
703 H6)))))))))))) c y H0))) H))))).
708 theorem csuba_gen_abbr_rev:
709 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c
710 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c (CHead d2
711 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
712 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abst)
713 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
714 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
715 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
716 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Bind Void)
717 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))))
719 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
720 (H: (csuba g c (CHead d1 (Bind Abbr) u1))).(insert_eq C (CHead d1 (Bind Abbr)
721 u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(or3 (ex2 C (\lambda
722 (d2: C).(eq C c (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
723 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
724 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
725 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
726 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
727 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
728 C c (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
729 d1)))))) (\lambda (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda
730 (c0: C).(\lambda (c1: C).((eq C c1 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C
731 (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
732 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
733 C c0 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
734 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
735 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
736 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
737 C c0 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
738 d2 d1)))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind
739 Abbr) u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C
740 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
741 \Rightarrow False])) I (CHead d1 (Bind Abbr) u1) H1) in (False_ind (or3 (ex2
742 C (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
743 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
744 (_: A).(eq C (CSort n) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
745 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
746 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
747 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
748 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Bind Void)
749 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) H2)))) (\lambda
750 (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C
751 c2 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c1
752 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
753 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind
754 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
755 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
756 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
757 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2
758 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
759 d1)))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
760 (CHead d1 (Bind Abbr) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match
761 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
762 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3) in ((let H5
763 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
764 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
765 u) (CHead d1 (Bind Abbr) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
766 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
767 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3)
768 in (\lambda (H7: (eq K k (Bind Abbr))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
769 T u1 (\lambda (t: T).(or3 (ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead
770 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
771 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 k t) (CHead d2 (Bind
772 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
773 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
774 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
775 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 k t)
776 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
777 d1)))))) (eq_ind_r K (Bind Abbr) (\lambda (k0: K).(or3 (ex2 C (\lambda (d2:
778 C).(eq C (CHead c1 k0 u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
779 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
780 C (CHead c1 k0 u1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
781 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
782 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
783 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2:
784 C).(\lambda (u2: T).(eq C (CHead c1 k0 u1) (CHead d2 (Bind Void) u2))))
785 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (let H9 \def (eq_ind C
786 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C
787 (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
788 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
789 C c1 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
790 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
791 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
792 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
793 C c1 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
794 d2 d1))))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba
795 g c1 c0)) H1 d1 H8) in (or3_intro0 (ex2 C (\lambda (d2: C).(eq C (CHead c1
796 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
797 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
798 (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
799 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
800 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
801 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
802 (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2
803 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
804 (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind
805 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1
806 (Bind Abbr) u1)) H10)))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
807 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
808 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c1 (CHead
809 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
810 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
811 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
812 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
813 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
814 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Bind Void)
815 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))).(\lambda (b:
816 B).(\lambda (H3: (not (eq B b Void))).(\lambda (u0: T).(\lambda (u2:
817 T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr)
818 u1))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
819 (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0]))
820 (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr) u1) H4) in ((let H6 \def
821 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
822 [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return
823 (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
824 b])])) (CHead c2 (Bind b) u2) (CHead d1 (Bind Abbr) u1) H4) in ((let H7 \def
825 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
826 [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b)
827 u2) (CHead d1 (Bind Abbr) u1) H4) in (\lambda (H8: (eq B b Abbr)).(\lambda
828 (H9: (eq C c2 d1)).(let H10 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0
829 Void))) H3 Abbr H8) in (let H11 \def (eq_ind C c2 (\lambda (c0: C).((eq C c0
830 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c1 (CHead
831 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
832 (d2: C).(\lambda (u3: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
833 u3))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
834 (\lambda (d2: C).(\lambda (u3: T).(\lambda (a: A).(arity g d2 u3 (asucc g
835 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
836 (ex2_2 C T (\lambda (d2: C).(\lambda (u3: T).(eq C c1 (CHead d2 (Bind Void)
837 u3)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) H2 d1 H9) in
838 (let H12 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H9) in
839 (or3_intro2 (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void) u0) (CHead d2
840 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
841 (d2: C).(\lambda (u3: T).(\lambda (_: A).(eq C (CHead c1 (Bind Void) u0)
842 (CHead d2 (Bind Abst) u3))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
843 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u3: T).(\lambda (a:
844 A).(arity g d2 u3 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
845 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u3: T).(eq
846 C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void) u3)))) (\lambda (d2:
847 C).(\lambda (_: T).(csuba g d2 d1)))) (ex2_2_intro C T (\lambda (d2:
848 C).(\lambda (u3: T).(eq C (CHead c1 (Bind Void) u0) (CHead d2 (Bind Void)
849 u3)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) c1 u0 (refl_equal C
850 (CHead c1 (Bind Void) u0)) H12)))))))) H6)) H5))))))))))) (\lambda (c1:
851 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
852 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c1 (CHead
853 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
854 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
855 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
856 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
857 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
858 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Bind Void)
859 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))).(\lambda (t:
860 T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc g a))).(\lambda (u:
861 T).(\lambda (H4: (arity g c2 u a)).(\lambda (H5: (eq C (CHead c2 (Bind Abbr)
862 u) (CHead d1 (Bind Abbr) u1))).(let H6 \def (f_equal C C (\lambda (e:
863 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 |
864 (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind Abbr) u) (CHead d1 (Bind
865 Abbr) u1) H5) in ((let H7 \def (f_equal C T (\lambda (e: C).(match e in C
866 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0)
867 \Rightarrow t0])) (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1) H5) in
868 (\lambda (H8: (eq C c2 d1)).(let H9 \def (eq_ind T u (\lambda (t0: T).(arity
869 g c2 t0 a)) H4 u1 H7) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(arity g
870 c0 u1 a)) H9 d1 H8) in (let H11 \def (eq_ind C c2 (\lambda (c0: C).((eq C c0
871 (CHead d1 (Bind Abbr) u1)) \to (or3 (ex2 C (\lambda (d2: C).(eq C c1 (CHead
872 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
873 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
874 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
875 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g
876 a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1
877 a0))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Bind
878 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) H2 d1 H8)
879 in (let H12 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in
880 (or3_intro1 (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2
881 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
882 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t)
883 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
884 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
885 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
886 (a0: A).(arity g d1 u1 a0))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
887 T).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2:
888 C).(\lambda (_: T).(csuba g d2 d1)))) (ex4_3_intro C T A (\lambda (d2:
889 C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t) (CHead d2
890 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
891 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
892 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1
893 u1 a0)))) c1 t a (refl_equal C (CHead c1 (Bind Abst) t)) H12 H3 H10))))))))
894 H6)))))))))))) c y H0))) H))))).
899 theorem csuba_gen_flat_rev:
900 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
901 (f: F).((csuba g c (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2:
902 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
903 C).(\lambda (_: T).(csuba g d2 d1)))))))))
905 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
906 (f: F).(\lambda (H: (csuba g c (CHead d1 (Flat f) u1))).(insert_eq C (CHead
907 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2_2 C T
908 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
909 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (y: C).(\lambda (H0:
910 (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c1
911 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
912 C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
913 d1))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
914 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
915 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
916 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
917 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
918 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) H2)))) (\lambda (c1:
919 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
920 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
921 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
922 d1))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
923 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
924 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
925 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
926 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
927 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
928 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
929 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
930 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in
931 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r T u1
932 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1
933 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
934 d1))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
935 C).(\lambda (u2: T).(eq C (CHead c1 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
936 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (let H9 \def (eq_ind C c2
937 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
938 (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2:
939 C).(\lambda (_: T).(csuba g d2 d1)))))) H2 d1 H8) in (let H10 \def (eq_ind C
940 c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (ex2_2_intro C T (\lambda
941 (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Flat f) u1) (CHead d2 (Flat f)
942 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) c1 u1 (refl_equal C
943 (CHead c1 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
944 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2
945 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
946 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
947 d1))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u0:
948 T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c2 (Bind b) u2) (CHead d1
949 (Flat f) u1))).(let H5 \def (eq_ind C (CHead c2 (Bind b) u2) (\lambda (ee:
950 C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
951 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
952 with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead d1
953 (Flat f) u1) H4) in (False_ind (ex2_2 C T (\lambda (d2: C).(\lambda (u3:
954 T).(eq C (CHead c1 (Bind Void) u0) (CHead d2 (Flat f) u3)))) (\lambda (d2:
955 C).(\lambda (_: T).(csuba g d2 d1)))) H5))))))))))) (\lambda (c1: C).(\lambda
956 (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Flat
957 f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2
958 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
959 d1))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
960 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
961 (CHead c2 (Bind Abbr) u) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
962 (CHead c2 (Bind Abbr) u) (\lambda (ee: C).(match ee in C return (\lambda (_:
963 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
964 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
965 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
966 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2
967 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
968 H6)))))))))))) c y H0))) H)))))).
973 theorem csuba_gen_bind_rev:
974 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
975 (v1: T).((csuba g c2 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
976 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
977 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))))))
979 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
980 (v1: T).(\lambda (H: (csuba g c2 (CHead e1 (Bind b1) v1))).(insert_eq C
981 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c2 c)) (\lambda (_:
982 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
983 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
984 T).(csuba g e2 e1)))))) (\lambda (y: C).(\lambda (H0: (csuba g c2
985 y)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c0 (CHead e1 (Bind
986 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
987 T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
988 C).(\lambda (_: T).(csuba g e2 e1)))))))) (\lambda (n: nat).(\lambda (H1: (eq
989 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
990 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
991 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
992 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
993 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
994 (e2: C).(\lambda (_: T).(csuba g e2 e1))))) H2)))) (\lambda (c1: C).(\lambda
995 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3 (CHead e1
996 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
997 (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
998 C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (k: K).(\lambda (u:
999 T).(\lambda (H3: (eq C (CHead c3 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
1000 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
1001 [(CSort _) \Rightarrow c3 | (CHead c _ _) \Rightarrow c])) (CHead c3 k u)
1002 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
1003 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
1004 (CHead _ k0 _) \Rightarrow k0])) (CHead c3 k u) (CHead e1 (Bind b1) v1) H3)
1005 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
1006 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
1007 (CHead c3 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
1008 b1))).(\lambda (H8: (eq C c3 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
1009 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k t)
1010 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
1011 T).(csuba g e2 e1)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
1012 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k0 v1)
1013 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
1014 T).(csuba g e2 e1)))))) (let H9 \def (eq_ind C c3 (\lambda (c: C).((eq C c
1015 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
1016 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
1017 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1 H8) in (let
1018 H10 \def (eq_ind C c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H8) in
1019 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
1020 (CHead c1 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
1021 (e2: C).(\lambda (_: T).(csuba g e2 e1)))) b1 c1 v1 (refl_equal C (CHead c1
1022 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
1023 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3
1024 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
1025 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
1026 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (b:
1027 B).(\lambda (H3: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
1028 T).(\lambda (H4: (eq C (CHead c3 (Bind b) u2) (CHead e1 (Bind b1) v1))).(let
1029 H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
1030 with [(CSort _) \Rightarrow c3 | (CHead c _ _) \Rightarrow c])) (CHead c3
1031 (Bind b) u2) (CHead e1 (Bind b1) v1) H4) in ((let H6 \def (f_equal C B
1032 (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
1033 \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_:
1034 K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow b])])) (CHead c3
1035 (Bind b) u2) (CHead e1 (Bind b1) v1) H4) in ((let H7 \def (f_equal C T
1036 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
1037 \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c3 (Bind b) u2) (CHead
1038 e1 (Bind b1) v1) H4) in (\lambda (H8: (eq B b b1)).(\lambda (H9: (eq C c3
1039 e1)).(let H10 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Void))) H3 b1
1040 H8) in (let H11 \def (eq_ind C c3 (\lambda (c: C).((eq C c (CHead e1 (Bind
1041 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
1042 T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
1043 C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1 H9) in (let H12 \def (eq_ind C
1044 c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H9) in (ex2_3_intro B C T (\lambda
1045 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind Void) u1)
1046 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
1047 T).(csuba g e2 e1)))) Void c1 u1 (refl_equal C (CHead c1 (Bind Void) u1))
1048 H12))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H1:
1049 (csuba g c1 c3)).(\lambda (H2: (((eq C c3 (CHead e1 (Bind b1) v1)) \to (ex2_3
1050 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c1 (CHead e2
1051 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
1052 e2 e1)))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t
1053 (asucc g a))).(\lambda (u: T).(\lambda (H4: (arity g c3 u a)).(\lambda (H5:
1054 (eq C (CHead c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1))).(let H6 \def
1055 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
1056 [(CSort _) \Rightarrow c3 | (CHead c _ _) \Rightarrow c])) (CHead c3 (Bind
1057 Abbr) u) (CHead e1 (Bind b1) v1) H5) in ((let H7 \def (f_equal C B (\lambda
1058 (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
1059 Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
1060 [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead c3 (Bind
1061 Abbr) u) (CHead e1 (Bind b1) v1) H5) in ((let H8 \def (f_equal C T (\lambda
1062 (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u
1063 | (CHead _ _ t0) \Rightarrow t0])) (CHead c3 (Bind Abbr) u) (CHead e1 (Bind
1064 b1) v1) H5) in (\lambda (H9: (eq B Abbr b1)).(\lambda (H10: (eq C c3
1065 e1)).(let H11 \def (eq_ind T u (\lambda (t0: T).(arity g c3 t0 a)) H4 v1 H8)
1066 in (let H12 \def (eq_ind C c3 (\lambda (c: C).(arity g c v1 a)) H11 e1 H10)
1067 in (let H13 \def (eq_ind C c3 (\lambda (c: C).((eq C c (CHead e1 (Bind b1)
1068 v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq
1069 C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda
1070 (_: T).(csuba g e2 e1))))))) H2 e1 H10) in (let H14 \def (eq_ind C c3
1071 (\lambda (c: C).(csuba g c1 c)) H1 e1 H10) in (let H15 \def (eq_ind_r B b1
1072 (\lambda (b: B).((eq C e1 (CHead e1 (Bind b) v1)) \to (ex2_3 B C T (\lambda
1073 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2)
1074 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2
1075 e1))))))) H13 Abbr H9) in (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2:
1076 C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2 (Bind b2)
1077 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))
1078 Abst c1 t (refl_equal C (CHead c1 (Bind Abst) t)) H14))))))))) H7))
1079 H6)))))))))))) c2 y H0))) H)))))).
projects / helm.git / blob