1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "LambdaDelta-1/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 (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
63 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
64 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abbr) u))).(let H6 \def (eq_ind C
65 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
66 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
67 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
68 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
69 True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
70 (Bind Abbr) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2
71 (Bind Abbr) u0) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))
72 H6)))))))))))) y c H0))) H))))).
74 theorem csuba_gen_void:
75 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
76 (CHead d1 (Bind Void) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
77 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
79 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
80 (csuba g (CHead d1 (Bind Void) u) c)).(insert_eq C (CHead d1 (Bind Void) u)
81 (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
82 C c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (\lambda
83 (y: C).(\lambda (H0: (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda
84 (c1: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
85 c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda
86 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H2
87 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
88 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
89 False])) I (CHead d1 (Bind Void) u) H1) in (False_ind (ex2 C (\lambda (d2:
90 C).(eq C (CSort n) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
91 d2))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
92 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
93 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
94 d2)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c1 k u0)
95 (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
96 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
97 _) \Rightarrow c0])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H3) in ((let H5
98 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
99 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
100 u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
101 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
102 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H3)
103 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r
104 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k t) (CHead d2
105 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (eq_ind_r K (Bind Void)
106 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u) (CHead d2
107 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H9 \def (eq_ind C
108 c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
109 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
110 d2))))) H2 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0
111 c2)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Void)
112 u) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)) c2
113 (refl_equal C (CHead c2 (Bind Void) u)) H10))) k H7) u0 H6)))) H5))
114 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
115 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
116 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
117 d2)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
118 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
119 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Void) u))).(let H6 \def (eq_ind C
120 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
121 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
122 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
123 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
124 True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
125 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2
126 (Bind Abbr) u0) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))
127 H6)))))))))))) y c H0))) H))))).
129 theorem csuba_gen_abst:
130 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
131 (CHead d1 (Bind Abst) u1) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead
132 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
133 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
134 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
135 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
136 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
139 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
140 (H: (csuba g (CHead d1 (Bind Abst) u1) c)).(insert_eq C (CHead d1 (Bind Abst)
141 u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
142 C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
143 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
144 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
145 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
146 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
147 A).(arity g d2 u2 a))))))) (\lambda (y: C).(\lambda (H0: (csuba g y
148 c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0 (CHead d1 (Bind
149 Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst)
150 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
151 C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abbr) u2)))))
152 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
153 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
154 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))
155 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst)
156 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
157 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
158 \Rightarrow False])) I (CHead d1 (Bind Abst) u1) H1) in (False_ind (or (ex2 C
159 (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
160 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
161 (_: A).(eq C (CSort n) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
162 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
163 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
164 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) H2))))
165 (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda
166 (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2:
167 C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
168 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
169 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
170 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
171 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
172 A).(arity g d2 u2 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3:
173 (eq C (CHead c1 k u) (CHead d1 (Bind Abst) u1))).(let H4 \def (f_equal C C
174 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
175 \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 k u) (CHead d1
176 (Bind Abst) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in
177 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
178 \Rightarrow k0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H3) in ((let H6
179 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
180 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u)
181 (CHead d1 (Bind Abst) u1) H3) in (\lambda (H7: (eq K k (Bind Abst))).(\lambda
182 (H8: (eq C c1 d1)).(eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2:
183 C).(eq C (CHead c2 k t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
184 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
185 (CHead c2 k t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
186 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
187 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
188 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (eq_ind_r K (Bind Abst)
189 (\lambda (k0: K).(or (ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u1) (CHead d2
190 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
191 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 k0 u1) (CHead d2
192 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
193 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
194 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
195 u2 a))))))) (let H9 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
196 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
197 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
198 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
199 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
200 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
201 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))) H2
202 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1
203 H8) in (or_introl (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1)
204 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
205 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst)
206 u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
207 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
208 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
209 (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2
210 (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
211 c2 (refl_equal C (CHead c2 (Bind Abst) u1)) H10)))) k H7) u H6)))) H5))
212 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
213 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C
214 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
215 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
216 C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
217 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
218 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
219 (a: A).(arity g d2 u2 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda
220 (H3: (arity g c1 t (asucc g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u
221 a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst)
222 u1))).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
223 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
224 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H5) in ((let H7 \def
225 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
226 [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c1 (Bind
227 Abst) t) (CHead d1 (Bind Abst) u1) H5) in (\lambda (H8: (eq C c1 d1)).(let H9
228 \def (eq_ind T t (\lambda (t0: T).(arity g c1 t0 (asucc g a))) H3 u1 H7) in
229 (let H10 \def (eq_ind C c1 (\lambda (c0: C).(arity g c0 u1 (asucc g a))) H9
230 d1 H8) in (let H11 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
231 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
232 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
233 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
234 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
235 (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0)))))
236 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0))))))))
237 H2 d1 H8) in (let H12 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1
238 d1 H8) in (or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u)
239 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
240 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr)
241 u) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
242 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
243 A).(arity g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
244 (a0: A).(arity g d2 u2 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda
245 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr)
246 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
247 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g
248 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
249 a0)))) c2 u a (refl_equal C (CHead c2 (Bind Abbr) u)) H12 H10 H4))))))))
250 H6)))))))))))) y c H0))) H))))).
252 theorem csuba_gen_flat:
253 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
254 (f: F).((csuba g (CHead d1 (Flat f) u1) c) \to (ex2_2 C T (\lambda (d2:
255 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
256 C).(\lambda (_: T).(csuba g d1 d2)))))))))
258 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
259 (f: F).(\lambda (H: (csuba g (CHead d1 (Flat f) u1) c)).(insert_eq C (CHead
260 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2_2 C T
261 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
262 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (\lambda (y: C).(\lambda (H0:
263 (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0
264 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
265 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
266 d2))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
267 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
268 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
269 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
270 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
271 (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))) H2)))) (\lambda (c1:
272 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c1
273 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
274 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
275 d2))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
276 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
277 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
278 _) \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
279 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
280 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
281 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
282 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
283 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in
284 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r T u1
285 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2
286 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
287 d2))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
288 C).(\lambda (u2: T).(eq C (CHead c2 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
289 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (let H9 \def (eq_ind C c1
290 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
291 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
292 C).(\lambda (_: T).(csuba g d1 d2)))))) H2 d1 H8) in (let H10 \def (eq_ind C
293 c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1 H8) in (ex2_2_intro C T (\lambda
294 (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Flat f) u1) (CHead d2 (Flat f)
295 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))) c2 u1 (refl_equal C
296 (CHead c2 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
297 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c1
298 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
299 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
300 d2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
301 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
302 (CHead c1 (Bind Abst) t) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
303 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
304 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
305 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
306 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
307 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
308 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))
309 H6)))))))))))) y c H0))) H)))))).
311 theorem csuba_gen_bind:
312 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
313 (v1: T).((csuba g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
314 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
315 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
317 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
318 (v1: T).(\lambda (H: (csuba g (CHead e1 (Bind b1) v1) c2)).(insert_eq C
319 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c c2)) (\lambda (_:
320 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
321 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
322 T).(csuba g e1 e2)))))) (\lambda (y: C).(\lambda (H0: (csuba g y
323 c2)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind
324 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
325 T).(eq C c0 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
326 C).(\lambda (_: T).(csuba g e1 e2)))))))) (\lambda (n: nat).(\lambda (H1: (eq
327 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
328 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
329 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
330 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
331 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
332 (e2: C).(\lambda (_: T).(csuba g e1 e2))))) H2)))) (\lambda (c1: C).(\lambda
333 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1
334 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
335 (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
336 C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (k: K).(\lambda (u:
337 T).(\lambda (H3: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
338 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
339 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k u)
340 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
341 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
342 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H3)
343 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
344 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
345 (CHead c1 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
346 b1))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
347 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k t)
348 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
349 T).(csuba g e1 e2)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
350 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k0 v1)
351 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
352 T).(csuba g e1 e2)))))) (let H9 \def (eq_ind C c1 (\lambda (c: C).((eq C c
353 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
354 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
355 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H2 e1 H8) in (let
356 H10 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c3)) H1 e1 H8) in
357 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
358 (CHead c3 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
359 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) b1 c3 v1 (refl_equal C (CHead c3
360 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
361 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1
362 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
363 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
364 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (t:
365 T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc g a))).(\lambda (u:
366 T).(\lambda (_: (arity g c3 u a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst)
367 t) (CHead e1 (Bind b1) v1))).(let H6 \def (f_equal C C (\lambda (e: C).(match
368 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c _
369 _) \Rightarrow c])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in
370 ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
371 C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
372 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
373 \Rightarrow Abst])])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in
374 ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
375 C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead
376 c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in (\lambda (H9: (eq B Abst
377 b1)).(\lambda (H10: (eq C c1 e1)).(let H11 \def (eq_ind T t (\lambda (t0:
378 T).(arity g c1 t0 (asucc g a))) H3 v1 H8) in (let H12 \def (eq_ind C c1
379 (\lambda (c: C).(arity g c v1 (asucc g a))) H11 e1 H10) in (let H13 \def
380 (eq_ind C c1 (\lambda (c: C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C
381 T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind
382 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
383 e2))))))) H2 e1 H10) in (let H14 \def (eq_ind C c1 (\lambda (c: C).(csuba g c
384 c3)) H1 e1 H10) in (let H15 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1
385 (CHead e1 (Bind b) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
386 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
387 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H13 Abst H9) in
388 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
389 (CHead c3 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
390 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) Abbr c3 u (refl_equal C (CHead c3
391 (Bind Abbr) u)) H14))))))))) H7)) H6)))))))))))) y c2 H0))) H)))))).
393 theorem csuba_gen_abst_rev:
394 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
395 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
396 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
398 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
399 (csuba g c (CHead d1 (Bind Abst) u))).(insert_eq C (CHead d1 (Bind Abst) u)
400 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
401 C c (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (\lambda
402 (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda
403 (c1: C).((eq C c1 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C
404 c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda
405 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst) u))).(let H2
406 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
407 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
408 False])) I (CHead d1 (Bind Abst) u) H1) in (False_ind (ex2 C (\lambda (d2:
409 C).(eq C (CSort n) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
410 d1))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
411 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
412 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
413 d1)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k u0)
414 (CHead d1 (Bind Abst) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
415 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
416 _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3) in ((let H5
417 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
418 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
419 u0) (CHead d1 (Bind Abst) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
420 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
421 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3)
422 in (\lambda (H7: (eq K k (Bind Abst))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
423 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead d2
424 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (eq_ind_r K (Bind Abst)
425 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k0 u) (CHead d2
426 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H9 \def (eq_ind C
427 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
428 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
429 d1))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
430 c0)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst)
431 u) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) c1
432 (refl_equal C (CHead c1 (Bind Abst) u)) H10))) k H7) u0 H6)))) H5))
433 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
434 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
435 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
436 d1)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
437 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
438 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Abst) u))).(let H6 \def (eq_ind C
439 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
440 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
441 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
442 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
443 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
444 d1 (Bind Abst) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
445 (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
446 H6)))))))))))) c y H0))) H))))).
448 theorem csuba_gen_void_rev:
449 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
450 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
451 Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
453 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
454 (csuba g c (CHead d1 (Bind Void) u))).(insert_eq C (CHead d1 (Bind Void) u)
455 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
456 C c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (\lambda
457 (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda
458 (c1: C).((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
459 c0 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda
460 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H2
461 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
462 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
463 False])) I (CHead d1 (Bind Void) u) H1) in (False_ind (ex2 C (\lambda (d2:
464 C).(eq C (CSort n) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
465 d1))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
466 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
467 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
468 d1)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k u0)
469 (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
470 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
471 _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3) in ((let H5
472 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
473 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
474 u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
475 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
476 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3)
477 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
478 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead d2
479 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (eq_ind_r K (Bind Void)
480 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k0 u) (CHead d2
481 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H9 \def (eq_ind C
482 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
483 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
484 d1))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
485 c0)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void)
486 u) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)) c1
487 (refl_equal C (CHead c1 (Bind Void) u)) H10))) k H7) u0 H6)))) H5))
488 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
489 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
490 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
491 d1)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
492 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
493 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Void) u))).(let H6 \def (eq_ind C
494 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
495 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
496 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
497 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
498 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
499 d1 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
500 (Bind Abst) t) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))
501 H6)))))))))))) c y H0))) H))))).
503 theorem csuba_gen_abbr_rev:
504 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c
505 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
506 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
507 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abst)
508 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
509 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
510 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
513 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
514 (H: (csuba g c (CHead d1 (Bind Abbr) u1))).(insert_eq C (CHead d1 (Bind Abbr)
515 u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
516 C).(eq C c (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
517 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
518 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
519 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
520 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
521 (a: A).(arity g d1 u1 a))))))) (\lambda (y: C).(\lambda (H0: (csuba g c
522 y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c1 (CHead d1 (Bind
523 Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Abbr)
524 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
525 C).(\lambda (u2: T).(\lambda (_: A).(eq C c0 (CHead d2 (Bind Abst) u2)))))
526 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
527 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
528 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))))))
529 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abbr)
530 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
531 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
532 \Rightarrow False])) I (CHead d1 (Bind Abbr) u1) H1) in (False_ind (or (ex2 C
533 (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
534 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
535 (_: A).(eq C (CSort n) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
536 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
537 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
538 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) H2)))) (\lambda
539 (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C
540 c2 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead
541 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
542 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
543 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
544 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
545 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
546 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
547 (CHead d1 (Bind Abbr) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match
548 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
549 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3) in ((let H5
550 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
551 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
552 u) (CHead d1 (Bind Abbr) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
553 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
554 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3)
555 in (\lambda (H7: (eq K k (Bind Abbr))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
556 T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead
557 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
558 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 k t) (CHead d2 (Bind
559 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
560 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
561 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
562 u1 a))))))) (eq_ind_r K (Bind Abbr) (\lambda (k0: K).(or (ex2 C (\lambda (d2:
563 C).(eq C (CHead c1 k0 u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
564 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
565 C (CHead c1 k0 u1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
566 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
567 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
568 (_: T).(\lambda (a: A).(arity g d1 u1 a))))))) (let H9 \def (eq_ind C c2
569 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda
570 (d2: C).(eq C c1 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
571 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1
572 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
573 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
574 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
575 (a: A).(arity g d1 u1 a)))))))) H2 d1 H8) in (let H10 \def (eq_ind C c2
576 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (or_introl (ex2 C (\lambda
577 (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1))) (\lambda
578 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
579 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abst)
580 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
581 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
582 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
583 (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind
584 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1
585 (Bind Abbr) u1)) H10)))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
586 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
587 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2
588 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
589 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
590 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
591 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
592 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
593 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc
594 g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u a)).(\lambda (H5: (eq C
595 (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1))).(let H6 \def (f_equal C
596 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
597 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind Abbr) u)
598 (CHead d1 (Bind Abbr) u1) H5) in ((let H7 \def (f_equal C T (\lambda (e:
599 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
600 (CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind Abbr) u) (CHead d1 (Bind
601 Abbr) u1) H5) in (\lambda (H8: (eq C c2 d1)).(let H9 \def (eq_ind T u
602 (\lambda (t0: T).(arity g c2 t0 a)) H4 u1 H7) in (let H10 \def (eq_ind C c2
603 (\lambda (c0: C).(arity g c0 u1 a)) H9 d1 H8) in (let H11 \def (eq_ind C c2
604 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda
605 (d2: C).(eq C c1 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
606 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1
607 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
608 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
609 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
610 (a0: A).(arity g d1 u1 a0)))))))) H2 d1 H8) in (let H12 \def (eq_ind C c2
611 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (or_intror (ex2 C (\lambda
612 (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda
613 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
614 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst)
615 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
616 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g
617 a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1
618 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
619 A).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
620 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
621 C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g a0))))) (\lambda
622 (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 a0)))) c1 t a
623 (refl_equal C (CHead c1 (Bind Abst) t)) H12 H3 H10)))))))) H6)))))))))))) c y
626 theorem csuba_gen_flat_rev:
627 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
628 (f: F).((csuba g c (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2:
629 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
630 C).(\lambda (_: T).(csuba g d2 d1)))))))))
632 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
633 (f: F).(\lambda (H: (csuba g c (CHead d1 (Flat f) u1))).(insert_eq C (CHead
634 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2_2 C T
635 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
636 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (y: C).(\lambda (H0:
637 (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c1
638 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
639 C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
640 d1))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
641 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
642 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
643 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
644 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
645 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) H2)))) (\lambda (c1:
646 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
647 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
648 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
649 d1))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
650 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
651 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
652 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
653 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
654 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
655 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
656 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
657 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in
658 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r T u1
659 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1
660 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
661 d1))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
662 C).(\lambda (u2: T).(eq C (CHead c1 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
663 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (let H9 \def (eq_ind C c2
664 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
665 (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2:
666 C).(\lambda (_: T).(csuba g d2 d1)))))) H2 d1 H8) in (let H10 \def (eq_ind C
667 c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (ex2_2_intro C T (\lambda
668 (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Flat f) u1) (CHead d2 (Flat f)
669 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) c1 u1 (refl_equal C
670 (CHead c1 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
671 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2
672 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
673 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
674 d1))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
675 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
676 (CHead c2 (Bind Abbr) u) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
677 (CHead c2 (Bind Abbr) u) (\lambda (ee: C).(match ee in C return (\lambda (_:
678 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
679 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
680 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
681 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2
682 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
683 H6)))))))))))) c y H0))) H)))))).
685 theorem csuba_gen_bind_rev:
686 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
687 (v1: T).((csuba g c2 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
688 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
689 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))))))
691 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
692 (v1: T).(\lambda (H: (csuba g c2 (CHead e1 (Bind b1) v1))).(insert_eq C
693 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c2 c)) (\lambda (_:
694 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
695 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
696 T).(csuba g e2 e1)))))) (\lambda (y: C).(\lambda (H0: (csuba g c2
697 y)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c0 (CHead e1 (Bind
698 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
699 T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
700 C).(\lambda (_: T).(csuba g e2 e1)))))))) (\lambda (n: nat).(\lambda (H1: (eq
701 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
702 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
703 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
704 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
705 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
706 (e2: C).(\lambda (_: T).(csuba g e2 e1))))) H2)))) (\lambda (c1: C).(\lambda
707 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3 (CHead e1
708 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
709 (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
710 C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (k: K).(\lambda (u:
711 T).(\lambda (H3: (eq C (CHead c3 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
712 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
713 [(CSort _) \Rightarrow c3 | (CHead c _ _) \Rightarrow c])) (CHead c3 k u)
714 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
715 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
716 (CHead _ k0 _) \Rightarrow k0])) (CHead c3 k u) (CHead e1 (Bind b1) v1) H3)
717 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
718 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
719 (CHead c3 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
720 b1))).(\lambda (H8: (eq C c3 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
721 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k t)
722 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
723 T).(csuba g e2 e1)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
724 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k0 v1)
725 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
726 T).(csuba g e2 e1)))))) (let H9 \def (eq_ind C c3 (\lambda (c: C).((eq C c
727 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
728 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
729 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1 H8) in (let
730 H10 \def (eq_ind C c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H8) in
731 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
732 (CHead c1 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
733 (e2: C).(\lambda (_: T).(csuba g e2 e1)))) b1 c1 v1 (refl_equal C (CHead c1
734 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
735 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3
736 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
737 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
738 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (t:
739 T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g a))).(\lambda (u:
740 T).(\lambda (H4: (arity g c3 u a)).(\lambda (H5: (eq C (CHead c3 (Bind Abbr)
741 u) (CHead e1 (Bind b1) v1))).(let H6 \def (f_equal C C (\lambda (e: C).(match
742 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c3 | (CHead c _
743 _) \Rightarrow c])) (CHead c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in
744 ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
745 C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k
746 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
747 \Rightarrow Abbr])])) (CHead c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in
748 ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
749 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
750 c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in (\lambda (H9: (eq B Abbr
751 b1)).(\lambda (H10: (eq C c3 e1)).(let H11 \def (eq_ind T u (\lambda (t0:
752 T).(arity g c3 t0 a)) H4 v1 H8) in (let H12 \def (eq_ind C c3 (\lambda (c:
753 C).(arity g c v1 a)) H11 e1 H10) in (let H13 \def (eq_ind C c3 (\lambda (c:
754 C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
755 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2)))))
756 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1
757 H10) in (let H14 \def (eq_ind C c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H10)
758 in (let H15 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1 (CHead e1 (Bind b)
759 v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq
760 C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda
761 (_: T).(csuba g e2 e1))))))) H13 Abbr H9) in (ex2_3_intro B C T (\lambda (b2:
762 B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2
763 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
764 e2 e1)))) Abst c1 t (refl_equal C (CHead c1 (Bind Abst) t)) H14))))))))) H7))
765 H6)))))))))))) c2 y H0))) H)))))).