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 *********************)
19 include "csuba/defs.ma".
21 theorem csuba_gen_abbr:
22 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
23 (CHead d1 (Bind Abbr) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
24 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
26 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
27 (csuba g (CHead d1 (Bind Abbr) u) c)).(let H0 \def (match H in csuba return
28 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0
29 (CHead d1 (Bind Abbr) u)) \to ((eq C c1 c) \to (ex2 C (\lambda (d2: C).(eq C
30 c (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))) with
31 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Bind
32 Abbr) u))).(\lambda (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort
33 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
34 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Abbr)
35 u) H0) in (False_ind ((eq C (CSort n) c) \to (ex2 C (\lambda (d2: C).(eq C c
36 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) H2)) H1))) |
37 (csuba_head c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0)
38 (CHead d1 (Bind Abbr) u))).(\lambda (H2: (eq C (CHead c2 k u0) c)).((let H3
39 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
40 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c1 k
41 u0) (CHead d1 (Bind Abbr) u) H1) in ((let H4 \def (f_equal C K (\lambda (e:
42 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
43 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H1)
44 in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
45 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
46 (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H1) in (eq_ind C d1 (\lambda (c0:
47 C).((eq K k (Bind Abbr)) \to ((eq T u0 u) \to ((eq C (CHead c2 k u0) c) \to
48 ((csuba g c0 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abbr)
49 u))) (\lambda (d2: C).(csuba g d1 d2)))))))) (\lambda (H6: (eq K k (Bind
50 Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T u0 u) \to ((eq C (CHead
51 c2 k0 u0) c) \to ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead
52 d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))) (\lambda (H7: (eq
53 T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c2 (Bind Abbr) t) c) \to
54 ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abbr)
55 u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (H8: (eq C (CHead c2
56 (Bind Abbr) u) c)).(eq_ind C (CHead c2 (Bind Abbr) u) (\lambda (c0:
57 C).((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
58 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))) (\lambda (H9: (csuba g d1
59 c2)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
60 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C (CHead c2
61 (Bind Abbr) u)) H9)) c H8)) u0 (sym_eq T u0 u H7))) k (sym_eq K k (Bind Abbr)
62 H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c2 H0 t a
63 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead d1
64 (Bind Abbr) u))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) c)).((let H5
65 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e: C).(match e in C return
66 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
67 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
68 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
69 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
70 \Rightarrow False])])) I (CHead d1 (Bind Abbr) u) H3) in (False_ind ((eq C
71 (CHead c2 (Bind Abbr) u0) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g
72 a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
73 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))) H5)) H4 H0 H1 H2)))])
74 in (H0 (refl_equal C (CHead d1 (Bind Abbr) u)) (refl_equal C c))))))).
76 theorem csuba_gen_void:
77 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
78 (CHead d1 (Bind Void) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
79 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
81 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
82 (csuba g (CHead d1 (Bind Void) u) c)).(let H0 \def (match H in csuba return
83 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0
84 (CHead d1 (Bind Void) u)) \to ((eq C c1 c) \to (ex2 C (\lambda (d2: C).(eq C
85 c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))) with
86 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Bind
87 Void) u))).(\lambda (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort
88 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
89 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Void)
90 u) H0) in (False_ind ((eq C (CSort n) c) \to (ex2 C (\lambda (d2: C).(eq C c
91 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) H2)) H1))) |
92 (csuba_head c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0)
93 (CHead d1 (Bind Void) u))).(\lambda (H2: (eq C (CHead c2 k u0) c)).((let H3
94 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
95 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c1 k
96 u0) (CHead d1 (Bind Void) u) H1) in ((let H4 \def (f_equal C K (\lambda (e:
97 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
98 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H1)
99 in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
100 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
101 (CHead c1 k u0) (CHead d1 (Bind Void) u) H1) in (eq_ind C d1 (\lambda (c0:
102 C).((eq K k (Bind Void)) \to ((eq T u0 u) \to ((eq C (CHead c2 k u0) c) \to
103 ((csuba g c0 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Void)
104 u))) (\lambda (d2: C).(csuba g d1 d2)))))))) (\lambda (H6: (eq K k (Bind
105 Void))).(eq_ind K (Bind Void) (\lambda (k0: K).((eq T u0 u) \to ((eq C (CHead
106 c2 k0 u0) c) \to ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead
107 d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2))))))) (\lambda (H7: (eq
108 T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c2 (Bind Void) t) c) \to
109 ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Void)
110 u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (H8: (eq C (CHead c2
111 (Bind Void) u) c)).(eq_ind C (CHead c2 (Bind Void) u) (\lambda (c0:
112 C).((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
113 Void) u))) (\lambda (d2: C).(csuba g d1 d2))))) (\lambda (H9: (csuba g d1
114 c2)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Void) u) (CHead d2
115 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C (CHead c2
116 (Bind Void) u)) H9)) c H8)) u0 (sym_eq T u0 u H7))) k (sym_eq K k (Bind Void)
117 H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c2 H0 t a
118 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead d1
119 (Bind Void) u))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) c)).((let H5
120 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e: C).(match e in C return
121 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
122 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
123 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
124 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
125 \Rightarrow False])])) I (CHead d1 (Bind Void) u) H3) in (False_ind ((eq C
126 (CHead c2 (Bind Abbr) u0) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g
127 a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
128 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2))))))) H5)) H4 H0 H1 H2)))])
129 in (H0 (refl_equal C (CHead d1 (Bind Void) u)) (refl_equal C c))))))).
131 theorem csuba_gen_abst:
132 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
133 (CHead d1 (Bind Abst) u1) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead
134 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
135 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
136 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
137 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
138 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
141 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
142 (H: (csuba g (CHead d1 (Bind Abst) u1) c)).(let H0 \def (match H in csuba
143 return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C
144 c0 (CHead d1 (Bind Abst) u1)) \to ((eq C c1 c) \to (or (ex2 C (\lambda (d2:
145 C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
146 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
147 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
148 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
149 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
150 A).(arity g d2 u2 a))))))))))) with [(csuba_sort n) \Rightarrow (\lambda (H0:
151 (eq C (CSort n) (CHead d1 (Bind Abst) u1))).(\lambda (H1: (eq C (CSort n)
152 c)).((let H2 \def (eq_ind C (CSort n) (\lambda (e: C).(match e in C return
153 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
154 \Rightarrow False])) I (CHead d1 (Bind Abst) u1) H0) in (False_ind ((eq C
155 (CSort n) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abst)
156 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
157 C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr) u2)))))
158 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
159 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
160 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))
161 H2)) H1))) | (csuba_head c1 c2 H0 k u) \Rightarrow (\lambda (H1: (eq C (CHead
162 c1 k u) (CHead d1 (Bind Abst) u1))).(\lambda (H2: (eq C (CHead c2 k u)
163 c)).((let H3 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
164 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
165 (CHead c1 k u) (CHead d1 (Bind Abst) u1) H1) in ((let H4 \def (f_equal C K
166 (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
167 \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead d1
168 (Bind Abst) u1) H1) in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in
169 C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _)
170 \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H1) in (eq_ind C
171 d1 (\lambda (c0: C).((eq K k (Bind Abst)) \to ((eq T u u1) \to ((eq C (CHead
172 c2 k u) c) \to ((csuba g c0 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c
173 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
174 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind
175 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
176 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
177 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
178 a))))))))))) (\lambda (H6: (eq K k (Bind Abst))).(eq_ind K (Bind Abst)
179 (\lambda (k0: K).((eq T u u1) \to ((eq C (CHead c2 k0 u) c) \to ((csuba g d1
180 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abst) u1)))
181 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
182 (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
183 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
184 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
185 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))) (\lambda
186 (H7: (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C (CHead c2 (Bind Abst)
187 t) c) \to ((csuba g d1 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
188 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
189 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
190 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
191 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
192 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
193 a))))))))) (\lambda (H8: (eq C (CHead c2 (Bind Abst) u1) c)).(eq_ind C (CHead
194 c2 (Bind Abst) u1) (\lambda (c0: C).((csuba g d1 c2) \to (or (ex2 C (\lambda
195 (d2: C).(eq C c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
196 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c0
197 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
198 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
199 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
200 A).(arity g d2 u2 a)))))))) (\lambda (H9: (csuba g d1 c2)).(or_introl (ex2 C
201 (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abst) u1)))
202 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
203 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abbr)
204 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
205 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
206 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
207 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead
208 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C
209 (CHead c2 (Bind Abst) u1)) H9))) c H8)) u (sym_eq T u u1 H7))) k (sym_eq K k
210 (Bind Abst) H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst
211 c1 c2 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst)
212 t) (CHead d1 (Bind Abst) u1))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u)
213 c)).((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
214 (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0]))
215 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H3) in ((let H6 \def
216 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
217 [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind
218 Abst) t) (CHead d1 (Bind Abst) u1) H3) in (eq_ind C d1 (\lambda (c0: C).((eq
219 T t u1) \to ((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g c0 c2) \to
220 ((arity g c0 t (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
221 (d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
222 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
223 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
224 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
225 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
226 A).(arity g d2 u2 a0)))))))))))) (\lambda (H7: (eq T t u1)).(eq_ind T u1
227 (\lambda (t0: T).((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g d1 c2) \to
228 ((arity g d1 t0 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
229 (d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
230 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
231 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
232 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
233 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
234 A).(arity g d2 u2 a0))))))))))) (\lambda (H8: (eq C (CHead c2 (Bind Abbr) u)
235 c)).(eq_ind C (CHead c2 (Bind Abbr) u) (\lambda (c0: C).((csuba g d1 c2) \to
236 ((arity g d1 u1 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
237 (d2: C).(eq C c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
238 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c0
239 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
240 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
241 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
242 A).(arity g d2 u2 a0)))))))))) (\lambda (H9: (csuba g d1 c2)).(\lambda (H10:
243 (arity g d1 u1 (asucc g a))).(\lambda (H11: (arity g c2 u a)).(or_intror (ex2
244 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abst) u1)))
245 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
246 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr)
247 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
248 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g
249 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
250 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
251 A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
252 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
253 C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0))))) (\lambda
254 (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0)))) c2 u a
255 (refl_equal C (CHead c2 (Bind Abbr) u)) H9 H10 H11))))) c H8)) t (sym_eq T t
256 u1 H7))) c1 (sym_eq C c1 d1 H6))) H5)) H4 H0 H1 H2)))]) in (H0 (refl_equal C
257 (CHead d1 (Bind Abst) u1)) (refl_equal C c))))))).
259 theorem csuba_gen_flat:
260 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
261 (f: F).((csuba g (CHead d1 (Flat f) u1) c) \to (ex2_2 C T (\lambda (d2:
262 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
263 C).(\lambda (_: T).(csuba g d1 d2)))))))))
265 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
266 (f: F).(\lambda (H: (csuba g (CHead d1 (Flat f) u1) c)).(let H0 \def (match H
267 in csuba return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0
268 c1)).((eq C c0 (CHead d1 (Flat f) u1)) \to ((eq C c1 c) \to (ex2_2 C T
269 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
270 (d2: C).(\lambda (_: T).(csuba g d1 d2))))))))) with [(csuba_sort n)
271 \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Flat f) u1))).(\lambda
272 (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort n) (\lambda (e:
273 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
274 True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Flat f) u1) H0) in
275 (False_ind ((eq C (CSort n) c) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
276 T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
277 g d1 d2))))) H2)) H1))) | (csuba_head c1 c2 H0 k u) \Rightarrow (\lambda (H1:
278 (eq C (CHead c1 k u) (CHead d1 (Flat f) u1))).(\lambda (H2: (eq C (CHead c2 k
279 u) c)).((let H3 \def (f_equal C T (\lambda (e: C).(match e in C return
280 (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow
281 t])) (CHead c1 k u) (CHead d1 (Flat f) u1) H1) in ((let H4 \def (f_equal C K
282 (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
283 \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead d1
284 (Flat f) u1) H1) in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C
285 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _)
286 \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Flat f) u1) H1) in (eq_ind C d1
287 (\lambda (c0: C).((eq K k (Flat f)) \to ((eq T u u1) \to ((eq C (CHead c2 k
288 u) c) \to ((csuba g c0 c2) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
289 T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
290 g d1 d2))))))))) (\lambda (H6: (eq K k (Flat f))).(eq_ind K (Flat f) (\lambda
291 (k0: K).((eq T u u1) \to ((eq C (CHead c2 k0 u) c) \to ((csuba g d1 c2) \to
292 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f)
293 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))))) (\lambda (H7:
294 (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C (CHead c2 (Flat f) t) c) \to
295 ((csuba g d1 c2) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c
296 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
297 d2))))))) (\lambda (H8: (eq C (CHead c2 (Flat f) u1) c)).(eq_ind C (CHead c2
298 (Flat f) u1) (\lambda (c0: C).((csuba g d1 c2) \to (ex2_2 C T (\lambda (d2:
299 C).(\lambda (u2: T).(eq C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2:
300 C).(\lambda (_: T).(csuba g d1 d2)))))) (\lambda (H9: (csuba g d1
301 c2)).(ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Flat
302 f) u1) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
303 d2))) c2 u1 (refl_equal C (CHead c2 (Flat f) u1)) H9)) c H8)) u (sym_eq T u
304 u1 H7))) k (sym_eq K k (Flat f) H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2
305 H0))) | (csuba_abst c1 c2 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C
306 (CHead c1 (Bind Abst) t) (CHead d1 (Flat f) u1))).(\lambda (H4: (eq C (CHead
307 c2 (Bind Abbr) u) c)).((let H5 \def (eq_ind C (CHead c1 (Bind Abst) t)
308 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
309 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
310 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
311 False])])) I (CHead d1 (Flat f) u1) H3) in (False_ind ((eq C (CHead c2 (Bind
312 Abbr) u) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity
313 g c2 u a) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2
314 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))))) H5))
315 H4 H0 H1 H2)))]) in (H0 (refl_equal C (CHead d1 (Flat f) u1)) (refl_equal C
318 theorem csuba_gen_bind:
319 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
320 (v1: T).((csuba g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
321 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
322 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
324 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
325 (v1: T).(\lambda (H: (csuba g (CHead e1 (Bind b1) v1) c2)).(let H0 \def
326 (match H in csuba return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csuba
327 ? c c0)).((eq C c (CHead e1 (Bind b1) v1)) \to ((eq C c0 c2) \to (ex2_3 B C T
328 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
329 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
330 e2)))))))))) with [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n)
331 (CHead e1 (Bind b1) v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def
332 (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
333 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
334 False])) I (CHead e1 (Bind b1) v1) H0) in (False_ind ((eq C (CSort n) c2) \to
335 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
336 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
337 T).(csuba g e1 e2)))))) H2)) H1))) | (csuba_head c1 c0 H0 k u) \Rightarrow
338 (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(\lambda (H2:
339 (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T (\lambda (e: C).(match e
340 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
341 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in ((let H4 \def
342 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
343 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u)
344 (CHead e1 (Bind b1) v1) H1) in ((let H5 \def (f_equal C C (\lambda (e:
345 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 |
346 (CHead c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in
347 (eq_ind C e1 (\lambda (c: C).((eq K k (Bind b1)) \to ((eq T u v1) \to ((eq C
348 (CHead c0 k u) c2) \to ((csuba g c c0) \to (ex2_3 B C T (\lambda (b2:
349 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
350 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
351 (\lambda (H6: (eq K k (Bind b1))).(eq_ind K (Bind b1) (\lambda (k0: K).((eq T
352 u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csuba g e1 c0) \to (ex2_3 B C T
353 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
354 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
355 e2))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
356 (CHead c0 (Bind b1) t) c2) \to ((csuba g e1 c0) \to (ex2_3 B C T (\lambda
357 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2)
358 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
359 e2)))))))) (\lambda (H8: (eq C (CHead c0 (Bind b1) v1) c2)).(eq_ind C (CHead
360 c0 (Bind b1) v1) (\lambda (c: C).((csuba g e1 c0) \to (ex2_3 B C T (\lambda
361 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
362 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))
363 (\lambda (H9: (csuba g e1 c0)).(let H10 \def (eq_ind_r C c2 (\lambda (c:
364 C).(csuba g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b1) v1) H8) in
365 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
366 (CHead c0 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
367 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) b1 c0 v1 (refl_equal C (CHead c0
368 (Bind b1) v1)) H9))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind b1)
369 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c0 H0 t a
370 H1 u H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead e1
371 (Bind b1) v1))).(\lambda (H4: (eq C (CHead c0 (Bind Abbr) u) c2)).((let H5
372 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
373 with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c1
374 (Bind Abst) t) (CHead e1 (Bind b1) v1) H3) in ((let H6 \def (f_equal C B
375 (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
376 \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k in K return (\lambda
377 (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])]))
378 (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H3) in ((let H7 \def
379 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
380 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind
381 Abst) t) (CHead e1 (Bind b1) v1) H3) in (eq_ind C e1 (\lambda (c: C).((eq B
382 Abst b1) \to ((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csuba
383 g c c0) \to ((arity g c t (asucc g a)) \to ((arity g c0 u a) \to (ex2_3 B C T
384 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
385 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
386 e2)))))))))))) (\lambda (H8: (eq B Abst b1)).(eq_ind B Abst (\lambda (_:
387 B).((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csuba g e1 c0)
388 \to ((arity g e1 t (asucc g a)) \to ((arity g c0 u a) \to (ex2_3 B C T
389 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
390 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
391 e2))))))))))) (\lambda (H9: (eq T t v1)).(eq_ind T v1 (\lambda (t0: T).((eq C
392 (CHead c0 (Bind Abbr) u) c2) \to ((csuba g e1 c0) \to ((arity g e1 t0 (asucc
393 g a)) \to ((arity g c0 u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
394 C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_:
395 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))))) (\lambda (H10:
396 (eq C (CHead c0 (Bind Abbr) u) c2)).(eq_ind C (CHead c0 (Bind Abbr) u)
397 (\lambda (c: C).((csuba g e1 c0) \to ((arity g e1 v1 (asucc g a)) \to ((arity
398 g c0 u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
399 T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
400 C).(\lambda (_: T).(csuba g e1 e2))))))))) (\lambda (H11: (csuba g e1
401 c0)).(\lambda (_: (arity g e1 v1 (asucc g a))).(\lambda (_: (arity g c0 u
402 a)).(let H14 \def (eq_ind_r C c2 (\lambda (c: C).(csuba g (CHead e1 (Bind b1)
403 v1) c)) H (CHead c0 (Bind Abbr) u) H10) in (let H15 \def (eq_ind_r B b1
404 (\lambda (b: B).(csuba g (CHead e1 (Bind b) v1) (CHead c0 (Bind Abbr) u)))
405 H14 Abst H8) in (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
406 (v2: T).(eq C (CHead c0 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda
407 (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))) Abbr c0 u
408 (refl_equal C (CHead c0 (Bind Abbr) u)) H11)))))) c2 H10)) t (sym_eq T t v1
409 H9))) b1 H8)) c1 (sym_eq C c1 e1 H7))) H6)) H5)) H4 H0 H1 H2)))]) in (H0
410 (refl_equal C (CHead e1 (Bind b1) v1)) (refl_equal C c2)))))))).
412 theorem csuba_gen_abst_rev:
413 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
414 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
415 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
417 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
418 (csuba g c (CHead d1 (Bind Abst) u))).(let H0 \def (match H in csuba return
419 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0 c)
420 \to ((eq C c1 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C c
421 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))) with
422 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) c)).(\lambda (H1:
423 (eq C (CSort n) (CHead d1 (Bind Abst) u))).(eq_ind C (CSort n) (\lambda (c0:
424 C).((eq C (CSort n) (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq
425 C c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))))) (\lambda
426 (H2: (eq C (CSort n) (CHead d1 (Bind Abst) u))).(let H3 \def (eq_ind C (CSort
427 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
428 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Abst)
429 u) H2) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind
430 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) H3))) c H0 H1))) | (csuba_head
431 c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0) c)).(\lambda
432 (H2: (eq C (CHead c2 k u0) (CHead d1 (Bind Abst) u))).(eq_ind C (CHead c1 k
433 u0) (\lambda (c0: C).((eq C (CHead c2 k u0) (CHead d1 (Bind Abst) u)) \to
434 ((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Abst)
435 u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda (H3: (eq C (CHead c2 k
436 u0) (CHead d1 (Bind Abst) u))).(let H4 \def (f_equal C T (\lambda (e:
437 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
438 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3)
439 in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
440 (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
441 (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3) in ((let H6 \def (f_equal C C
442 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
443 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1
444 (Bind Abst) u) H3) in (eq_ind C d1 (\lambda (c0: C).((eq K k (Bind Abst)) \to
445 ((eq T u0 u) \to ((csuba g c1 c0) \to (ex2 C (\lambda (d2: C).(eq C (CHead c1
446 k u0) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
447 (\lambda (H7: (eq K k (Bind Abst))).(eq_ind K (Bind Abst) (\lambda (k0:
448 K).((eq T u0 u) \to ((csuba g c1 d1) \to (ex2 C (\lambda (d2: C).(eq C (CHead
449 c1 k0 u0) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))))))
450 (\lambda (H8: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((csuba g c1 d1) \to
451 (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst)
452 u))) (\lambda (d2: C).(csuba g d2 d1))))) (\lambda (H9: (csuba g c1
453 d1)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) u) (CHead d2
454 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1
455 (Bind Abst) u)) H9)) u0 (sym_eq T u0 u H8))) k (sym_eq K k (Bind Abst) H7)))
456 c2 (sym_eq C c2 d1 H6))) H5)) H4))) c H1 H2 H0))) | (csuba_abst c1 c2 H0 t a
457 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t)
458 c)).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Abst)
459 u))).(eq_ind C (CHead c1 (Bind Abst) t) (\lambda (c0: C).((eq C (CHead c2
460 (Bind Abbr) u0) (CHead d1 (Bind Abst) u)) \to ((csuba g c1 c2) \to ((arity g
461 c1 t (asucc g a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c0
462 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))) (\lambda
463 (H5: (eq C (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Abst) u))).(let H6 \def
464 (eq_ind C (CHead c2 (Bind Abbr) u0) (\lambda (e: C).(match e in C return
465 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
466 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
467 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
468 True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _)
469 \Rightarrow False])])) I (CHead d1 (Bind Abst) u) H5) in (False_ind ((csuba g
470 c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity g c2 u0 a) \to (ex2 C
471 (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u)))
472 (\lambda (d2: C).(csuba g d2 d1)))))) H6))) c H3 H4 H0 H1 H2)))]) in (H0
473 (refl_equal C c) (refl_equal C (CHead d1 (Bind Abst) u)))))))).
475 theorem csuba_gen_void_rev:
476 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
477 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
478 Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
480 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
481 (csuba g c (CHead d1 (Bind Void) u))).(let H0 \def (match H in csuba return
482 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0 c)
483 \to ((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C c
484 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))) with
485 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) c)).(\lambda (H1:
486 (eq C (CSort n) (CHead d1 (Bind Void) u))).(eq_ind C (CSort n) (\lambda (c0:
487 C).((eq C (CSort n) (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq
488 C c0 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1))))) (\lambda
489 (H2: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H3 \def (eq_ind C (CSort
490 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
491 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Void)
492 u) H2) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind
493 Void) u))) (\lambda (d2: C).(csuba g d2 d1))) H3))) c H0 H1))) | (csuba_head
494 c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0) c)).(\lambda
495 (H2: (eq C (CHead c2 k u0) (CHead d1 (Bind Void) u))).(eq_ind C (CHead c1 k
496 u0) (\lambda (c0: C).((eq C (CHead c2 k u0) (CHead d1 (Bind Void) u)) \to
497 ((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Void)
498 u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda (H3: (eq C (CHead c2 k
499 u0) (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C T (\lambda (e:
500 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
501 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3)
502 in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
503 (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
504 (CHead c2 k u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C C
505 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
506 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1
507 (Bind Void) u) H3) in (eq_ind C d1 (\lambda (c0: C).((eq K k (Bind Void)) \to
508 ((eq T u0 u) \to ((csuba g c1 c0) \to (ex2 C (\lambda (d2: C).(eq C (CHead c1
509 k u0) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
510 (\lambda (H7: (eq K k (Bind Void))).(eq_ind K (Bind Void) (\lambda (k0:
511 K).((eq T u0 u) \to ((csuba g c1 d1) \to (ex2 C (\lambda (d2: C).(eq C (CHead
512 c1 k0 u0) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1))))))
513 (\lambda (H8: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((csuba g c1 d1) \to
514 (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void) t) (CHead d2 (Bind Void)
515 u))) (\lambda (d2: C).(csuba g d2 d1))))) (\lambda (H9: (csuba g c1
516 d1)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void) u) (CHead d2
517 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1
518 (Bind Void) u)) H9)) u0 (sym_eq T u0 u H8))) k (sym_eq K k (Bind Void) H7)))
519 c2 (sym_eq C c2 d1 H6))) H5)) H4))) c H1 H2 H0))) | (csuba_abst c1 c2 H0 t a
520 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t)
521 c)).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Void)
522 u))).(eq_ind C (CHead c1 (Bind Abst) t) (\lambda (c0: C).((eq C (CHead c2
523 (Bind Abbr) u0) (CHead d1 (Bind Void) u)) \to ((csuba g c1 c2) \to ((arity g
524 c1 t (asucc g a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c0
525 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))) (\lambda
526 (H5: (eq C (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Void) u))).(let H6 \def
527 (eq_ind C (CHead c2 (Bind Abbr) u0) (\lambda (e: C).(match e in C return
528 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
529 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
530 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
531 True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _)
532 \Rightarrow False])])) I (CHead d1 (Bind Void) u) H5) in (False_ind ((csuba g
533 c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity g c2 u0 a) \to (ex2 C
534 (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Void) u)))
535 (\lambda (d2: C).(csuba g d2 d1)))))) H6))) c H3 H4 H0 H1 H2)))]) in (H0
536 (refl_equal C c) (refl_equal C (CHead d1 (Bind Void) u)))))))).
538 theorem csuba_gen_abbr_rev:
539 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c
540 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
541 (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 c (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
548 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
549 (H: (csuba g c (CHead d1 (Bind Abbr) u1))).(let H0 \def (match H in csuba
550 return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C
551 c0 c) \to ((eq C c1 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2:
552 C).(eq C c (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
553 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
554 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
555 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
556 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
557 (a: A).(arity g d1 u1 a))))))))))) with [(csuba_sort n) \Rightarrow (\lambda
558 (H0: (eq C (CSort n) c)).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abbr)
559 u1))).(eq_ind C (CSort n) (\lambda (c0: C).((eq C (CSort n) (CHead d1 (Bind
560 Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Abbr)
561 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
562 C).(\lambda (u2: T).(\lambda (_: A).(eq C c0 (CHead d2 (Bind Abst) u2)))))
563 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
564 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
565 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))))
566 (\lambda (H2: (eq C (CSort n) (CHead d1 (Bind Abbr) u1))).(let H3 \def
567 (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
568 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
569 False])) I (CHead d1 (Bind Abbr) u1) H2) in (False_ind (or (ex2 C (\lambda
570 (d2: C).(eq C (CSort n) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g
571 d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
572 (CSort n) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
573 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
574 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
575 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) H3))) c H0 H1))) | (csuba_head
576 c1 c2 H0 k u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u) c)).(\lambda
577 (H2: (eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1))).(eq_ind C (CHead c1 k
578 u) (\lambda (c0: C).((eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1)) \to
579 ((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
580 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
581 C).(\lambda (u2: T).(\lambda (_: A).(eq C c0 (CHead d2 (Bind Abst) u2)))))
582 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
583 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
584 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))))))
585 (\lambda (H3: (eq C (CHead c2 k u) (CHead d1 (Bind Abbr) u1))).(let H4 \def
586 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
587 [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c2 k u)
588 (CHead d1 (Bind Abbr) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
589 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
590 (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3)
591 in ((let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
592 (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0]))
593 (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3) in (eq_ind C d1 (\lambda (c0:
594 C).((eq K k (Bind Abbr)) \to ((eq T u u1) \to ((csuba g c1 c0) \to (or (ex2 C
595 (\lambda (d2: C).(eq C (CHead c1 k u) (CHead d2 (Bind Abbr) u1))) (\lambda
596 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
597 T).(\lambda (_: A).(eq C (CHead c1 k u) (CHead d2 (Bind Abst) u2)))))
598 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
599 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
600 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))))))
601 (\lambda (H7: (eq K k (Bind Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0:
602 K).((eq T u u1) \to ((csuba g c1 d1) \to (or (ex2 C (\lambda (d2: C).(eq C
603 (CHead c1 k0 u) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
604 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
605 (CHead c1 k0 u) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
606 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
607 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
608 (_: T).(\lambda (a: A).(arity g d1 u1 a))))))))) (\lambda (H8: (eq T u
609 u1)).(eq_ind T u1 (\lambda (t: T).((csuba g c1 d1) \to (or (ex2 C (\lambda
610 (d2: C).(eq C (CHead c1 (Bind Abbr) t) (CHead d2 (Bind Abbr) u1))) (\lambda
611 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
612 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abbr) t) (CHead d2 (Bind Abst)
613 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
614 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
615 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
616 a)))))))) (\lambda (H9: (csuba g c1 d1)).(or_introl (ex2 C (\lambda (d2:
617 C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
618 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
619 (_: A).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abst) u2))))) (\lambda
620 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
621 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
622 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex_intro2 C
623 (\lambda (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1)))
624 (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1 (Bind Abbr) u1))
625 H9))) u (sym_eq T u u1 H8))) k (sym_eq K k (Bind Abbr) H7))) c2 (sym_eq C c2
626 d1 H6))) H5)) H4))) c H1 H2 H0))) | (csuba_abst c1 c2 H0 t a H1 u H2)
627 \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) c)).(\lambda (H4:
628 (eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1))).(eq_ind C (CHead
629 c1 (Bind Abst) t) (\lambda (c0: C).((eq C (CHead c2 (Bind Abbr) u) (CHead d1
630 (Bind Abbr) u1)) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g a)) \to
631 ((arity g c2 u a) \to (or (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
632 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
633 C).(\lambda (u2: T).(\lambda (_: A).(eq C c0 (CHead d2 (Bind Abst) u2)))))
634 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
635 (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g a0)))))
636 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 a0)))))))))))
637 (\lambda (H5: (eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1))).(let
638 H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
639 with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead c2
640 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1) H5) in ((let H7 \def (f_equal C C
641 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
642 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind Abbr) u)
643 (CHead d1 (Bind Abbr) u1) H5) in (eq_ind C d1 (\lambda (c0: C).((eq T u u1)
644 \to ((csuba g c1 c0) \to ((arity g c1 t (asucc g a)) \to ((arity g c0 u a)
645 \to (or (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2
646 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
647 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t)
648 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
649 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
650 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
651 (a0: A).(arity g d1 u1 a0))))))))))) (\lambda (H8: (eq T u u1)).(eq_ind T u1
652 (\lambda (t0: T).((csuba g c1 d1) \to ((arity g c1 t (asucc g a)) \to ((arity
653 g d1 t0 a) \to (or (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t)
654 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
655 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst)
656 t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
657 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
658 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
659 (a0: A).(arity g d1 u1 a0)))))))))) (\lambda (H9: (csuba g c1 d1)).(\lambda
660 (H10: (arity g c1 t (asucc g a))).(\lambda (H11: (arity g d1 u1
661 a)).(or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead
662 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
663 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t)
664 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
665 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
666 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
667 (a0: A).(arity g d1 u1 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda
668 (u2: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst)
669 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
670 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g
671 a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1
672 a0)))) c1 t a (refl_equal C (CHead c1 (Bind Abst) t)) H9 H10 H11))))) u
673 (sym_eq T u u1 H8))) c2 (sym_eq C c2 d1 H7))) H6))) c H3 H4 H0 H1 H2)))]) in
674 (H0 (refl_equal C c) (refl_equal C (CHead d1 (Bind Abbr) u1)))))))).
676 theorem csuba_gen_flat_rev:
677 \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
678 (f: F).((csuba g c (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2:
679 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
680 C).(\lambda (_: T).(csuba g d2 d1)))))))))
682 \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
683 (f: F).(\lambda (H: (csuba g c (CHead d1 (Flat f) u1))).(let H0 \def (match H
684 in csuba return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0
685 c1)).((eq C c0 c) \to ((eq C c1 (CHead d1 (Flat f) u1)) \to (ex2_2 C T
686 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
687 (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))) with [(csuba_sort n)
688 \Rightarrow (\lambda (H0: (eq C (CSort n) c)).(\lambda (H1: (eq C (CSort n)
689 (CHead d1 (Flat f) u1))).(eq_ind C (CSort n) (\lambda (c0: C).((eq C (CSort
690 n) (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
691 T).(eq C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
692 g d2 d1)))))) (\lambda (H2: (eq C (CSort n) (CHead d1 (Flat f) u1))).(let H3
693 \def (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
694 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
695 False])) I (CHead d1 (Flat f) u1) H2) in (False_ind (ex2_2 C T (\lambda (d2:
696 C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2)))) (\lambda (d2:
697 C).(\lambda (_: T).(csuba g d2 d1)))) H3))) c H0 H1))) | (csuba_head c1 c2 H0
698 k u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u) c)).(\lambda (H2: (eq C
699 (CHead c2 k u) (CHead d1 (Flat f) u1))).(eq_ind C (CHead c1 k u) (\lambda
700 (c0: C).((eq C (CHead c2 k u) (CHead d1 (Flat f) u1)) \to ((csuba g c1 c2)
701 \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c0 (CHead d2 (Flat f)
702 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) (\lambda (H3:
703 (eq C (CHead c2 k u) (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C T
704 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
705 \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Flat
706 f) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in C return
707 (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow
708 k0])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C C
709 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
710 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 k u) (CHead d1
711 (Flat f) u1) H3) in (eq_ind C d1 (\lambda (c0: C).((eq K k (Flat f)) \to ((eq
712 T u u1) \to ((csuba g c1 c0) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
713 T).(eq C (CHead c1 k u) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda
714 (_: T).(csuba g d2 d1)))))))) (\lambda (H7: (eq K k (Flat f))).(eq_ind K
715 (Flat f) (\lambda (k0: K).((eq T u u1) \to ((csuba g c1 d1) \to (ex2_2 C T
716 (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 k0 u) (CHead d2 (Flat f)
717 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) (\lambda (H8:
718 (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((csuba g c1 d1) \to (ex2_2 C T
719 (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Flat f) t) (CHead d2 (Flat
720 f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (\lambda (H9:
721 (csuba g c1 d1)).(ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(eq C
722 (CHead c1 (Flat f) u1) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda
723 (_: T).(csuba g d2 d1))) c1 u1 (refl_equal C (CHead c1 (Flat f) u1)) H9)) u
724 (sym_eq T u u1 H8))) k (sym_eq K k (Flat f) H7))) c2 (sym_eq C c2 d1 H6)))
725 H5)) H4))) c H1 H2 H0))) | (csuba_abst c1 c2 H0 t a H1 u H2) \Rightarrow
726 (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) c)).(\lambda (H4: (eq C (CHead
727 c2 (Bind Abbr) u) (CHead d1 (Flat f) u1))).(eq_ind C (CHead c1 (Bind Abst) t)
728 (\lambda (c0: C).((eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Flat f) u1)) \to
729 ((csuba g c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity g c2 u a) \to
730 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c0 (CHead d2 (Flat f)
731 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))) (\lambda (H5:
732 (eq C (CHead c2 (Bind Abbr) u) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind
733 C (CHead c2 (Bind Abbr) u) (\lambda (e: C).(match e in C return (\lambda (_:
734 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
735 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
736 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind ((csuba
737 g c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity g c2 u a) \to (ex2_2 C T
738 (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2
739 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) H6)))
740 c H3 H4 H0 H1 H2)))]) in (H0 (refl_equal C c) (refl_equal C (CHead d1 (Flat
743 theorem csuba_gen_bind_rev:
744 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
745 (v1: T).((csuba g c2 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
746 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
747 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))))))
749 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
750 (v1: T).(\lambda (H: (csuba g c2 (CHead e1 (Bind b1) v1))).(let H0 \def
751 (match H in csuba return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csuba
752 ? c c0)).((eq C c c2) \to ((eq C c0 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T
753 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
754 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2
755 e1)))))))))) with [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n)
756 c2)).(\lambda (H1: (eq C (CSort n) (CHead e1 (Bind b1) v1))).(eq_ind C (CSort
757 n) (\lambda (c: C).((eq C (CSort n) (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T
758 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind
759 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2
760 e1))))))) (\lambda (H2: (eq C (CSort n) (CHead e1 (Bind b1) v1))).(let H3
761 \def (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
762 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
763 False])) I (CHead e1 (Bind b1) v1) H2) in (False_ind (ex2_3 B C T (\lambda
764 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CSort n) (CHead e2 (Bind b2)
765 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))
766 H3))) c2 H0 H1))) | (csuba_head c1 c0 H0 k u) \Rightarrow (\lambda (H1: (eq C
767 (CHead c1 k u) c2)).(\lambda (H2: (eq C (CHead c0 k u) (CHead e1 (Bind b1)
768 v1))).(eq_ind C (CHead c1 k u) (\lambda (c: C).((eq C (CHead c0 k u) (CHead
769 e1 (Bind b1) v1)) \to ((csuba g c1 c0) \to (ex2_3 B C T (\lambda (b2:
770 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
771 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))))
772 (\lambda (H3: (eq C (CHead c0 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
773 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
774 [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c0 k u)
775 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
776 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
777 (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k u) (CHead e1 (Bind b1) v1) H3)
778 in ((let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
779 (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c]))
780 (CHead c0 k u) (CHead e1 (Bind b1) v1) H3) in (eq_ind C e1 (\lambda (c:
781 C).((eq K k (Bind b1)) \to ((eq T u v1) \to ((csuba g c1 c) \to (ex2_3 B C T
782 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k u)
783 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
784 T).(csuba g e2 e1))))))))) (\lambda (H7: (eq K k (Bind b1))).(eq_ind K (Bind
785 b1) (\lambda (k0: K).((eq T u v1) \to ((csuba g c1 e1) \to (ex2_3 B C T
786 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k0 u)
787 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
788 T).(csuba g e2 e1)))))))) (\lambda (H8: (eq T u v1)).(eq_ind T v1 (\lambda
789 (t: T).((csuba g c1 e1) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
790 C).(\lambda (v2: T).(eq C (CHead c1 (Bind b1) t) (CHead e2 (Bind b2) v2)))))
791 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))))
792 (\lambda (H9: (csuba g c1 e1)).(let H10 \def (eq_ind T u (\lambda (t: T).(eq
793 C (CHead c1 k t) c2)) H1 v1 H8) in (let H11 \def (eq_ind K k (\lambda (k0:
794 K).(eq C (CHead c1 k0 v1) c2)) H10 (Bind b1) H7) in (let H12 \def (eq_ind_r C
795 c2 (\lambda (c: C).(csuba g c (CHead e1 (Bind b1) v1))) H (CHead c1 (Bind b1)
796 v1) H11) in (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
797 (v2: T).(eq C (CHead c1 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda
798 (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))) b1 c1 v1
799 (refl_equal C (CHead c1 (Bind b1) v1)) H9))))) u (sym_eq T u v1 H8))) k
800 (sym_eq K k (Bind b1) H7))) c0 (sym_eq C c0 e1 H6))) H5)) H4))) c2 H1 H2
801 H0))) | (csuba_abst c1 c0 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C
802 (CHead c1 (Bind Abst) t) c2)).(\lambda (H4: (eq C (CHead c0 (Bind Abbr) u)
803 (CHead e1 (Bind b1) v1))).(eq_ind C (CHead c1 (Bind Abst) t) (\lambda (c:
804 C).((eq C (CHead c0 (Bind Abbr) u) (CHead e1 (Bind b1) v1)) \to ((csuba g c1
805 c0) \to ((arity g c1 t (asucc g a)) \to ((arity g c0 u a) \to (ex2_3 B C T
806 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind
807 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2
808 e1)))))))))) (\lambda (H5: (eq C (CHead c0 (Bind Abbr) u) (CHead e1 (Bind b1)
809 v1))).(let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
810 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0]))
811 (CHead c0 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in ((let H7 \def
812 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
813 [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k in K return
814 (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
815 Abbr])])) (CHead c0 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in ((let H8
816 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
817 with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0
818 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in (eq_ind C e1 (\lambda (c:
819 C).((eq B Abbr b1) \to ((eq T u v1) \to ((csuba g c1 c) \to ((arity g c1 t
820 (asucc g a)) \to ((arity g c u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda
821 (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2 (Bind b2)
822 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2
823 e1))))))))))) (\lambda (H9: (eq B Abbr b1)).(eq_ind B Abbr (\lambda (_:
824 B).((eq T u v1) \to ((csuba g c1 e1) \to ((arity g c1 t (asucc g a)) \to
825 ((arity g e1 u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
826 (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2 (Bind b2) v2))))) (\lambda
827 (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))))))) (\lambda
828 (H10: (eq T u v1)).(eq_ind T v1 (\lambda (t0: T).((csuba g c1 e1) \to ((arity
829 g c1 t (asucc g a)) \to ((arity g e1 t0 a) \to (ex2_3 B C T (\lambda (b2:
830 B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2
831 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
832 e2 e1))))))))) (\lambda (H11: (csuba g c1 e1)).(\lambda (_: (arity g c1 t
833 (asucc g a))).(\lambda (_: (arity g e1 v1 a)).(let H14 \def (eq_ind_r C c2
834 (\lambda (c: C).(csuba g c (CHead e1 (Bind b1) v1))) H (CHead c1 (Bind Abst)
835 t) H3) in (let H15 \def (eq_ind_r B b1 (\lambda (b: B).(csuba g (CHead c1
836 (Bind Abst) t) (CHead e1 (Bind b) v1))) H14 Abbr H9) in (ex2_3_intro B C T
837 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind
838 Abst) t) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
839 C).(\lambda (_: T).(csuba g e2 e1)))) Abst c1 t (refl_equal C (CHead c1 (Bind
840 Abst) t)) H11)))))) u (sym_eq T u v1 H10))) b1 H9)) c0 (sym_eq C c0 e1 H8)))
841 H7)) H6))) c2 H3 H4 H0 H1 H2)))]) in (H0 (refl_equal C c2) (refl_equal C
842 (CHead e1 (Bind b1) v1))))))))).
projects / helm.git / blob