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