1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1A/csubt/defs.ma".
19 implied rec lemma csubt_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
20 nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubt
21 g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (u: T).(P (CHead c1 k u)
22 (CHead c2 k u))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csubt g c1
23 c2) \to ((P c1 c2) \to (\forall (b: B).((not (eq B b Void)) \to (\forall (u1:
24 T).(\forall (u2: T).(P (CHead c1 (Bind Void) u1) (CHead c2 (Bind b)
25 u2))))))))))) (f2: (\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to ((P
26 c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to ((ty3 g c2 u
27 t) \to (P (CHead c1 (Bind Abst) t) (CHead c2 (Bind Abbr) u))))))))))) (c: C)
28 (c0: C) (c1: csubt g c c0) on c1: P c c0 \def match c1 with [(csubt_sort n)
29 \Rightarrow (f n) | (csubt_head c2 c3 c4 k u) \Rightarrow (f0 c2 c3 c4
30 ((csubt_ind g P f f0 f1 f2) c2 c3 c4) k u) | (csubt_void c2 c3 c4 b n u1 u2)
31 \Rightarrow (f1 c2 c3 c4 ((csubt_ind g P f f0 f1 f2) c2 c3 c4) b n u1 u2) |
32 (csubt_abst c2 c3 c4 u t t0 t1) \Rightarrow (f2 c2 c3 c4 ((csubt_ind g P f f0
33 f1 f2) c2 c3 c4) u t t0 t1)].
36 \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csubt g
37 (CHead e1 (Bind Abbr) v) c2) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2
38 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2)))))))
40 \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda
41 (H: (csubt g (CHead e1 (Bind Abbr) v) c2)).(insert_eq C (CHead e1 (Bind Abbr)
42 v) (\lambda (c: C).(csubt g c c2)) (\lambda (_: C).(ex2 C (\lambda (e2:
43 C).(eq C c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2))))
44 (\lambda (y: C).(\lambda (H0: (csubt g y c2)).(csubt_ind g (\lambda (c:
45 C).(\lambda (c0: C).((eq C c (CHead e1 (Bind Abbr) v)) \to (ex2 C (\lambda
46 (e2: C).(eq C c0 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1
47 e2)))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead e1 (Bind
48 Abbr) v))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee with
49 [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1
50 (Bind Abbr) v) H1) in (False_ind (ex2 C (\lambda (e2: C).(eq C (CSort n)
51 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2))) H2)))) (\lambda
52 (c1: C).(\lambda (c3: C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C
53 c1 (CHead e1 (Bind Abbr) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2
54 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (k:
55 K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u) (CHead e1 (Bind Abbr)
56 v))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
57 \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1
58 (Bind Abbr) v) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e
59 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
60 u) (CHead e1 (Bind Abbr) v) H3) in ((let H6 \def (f_equal C T (\lambda (e:
61 C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
62 (CHead c1 k u) (CHead e1 (Bind Abbr) v) H3) in (\lambda (H7: (eq K k (Bind
63 Abbr))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v (\lambda (t: T).(ex2 C
64 (\lambda (e2: C).(eq C (CHead c3 k t) (CHead e2 (Bind Abbr) v))) (\lambda
65 (e2: C).(csubt g e1 e2)))) (eq_ind_r K (Bind Abbr) (\lambda (k0: K).(ex2 C
66 (\lambda (e2: C).(eq C (CHead c3 k0 v) (CHead e2 (Bind Abbr) v))) (\lambda
67 (e2: C).(csubt g e1 e2)))) (let H9 \def (eq_ind C c1 (\lambda (c: C).((eq C c
68 (CHead e1 (Bind Abbr) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2
69 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2))))) H2 e1 H8) in (let H10
70 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c3)) H1 e1 H8) in (ex_intro2 C
71 (\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) v) (CHead e2 (Bind Abbr) v)))
72 (\lambda (e2: C).(csubt g e1 e2)) c3 (refl_equal C (CHead c3 (Bind Abbr) v))
73 H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda (c3:
74 C).(\lambda (_: (csubt g c1 c3)).(\lambda (_: (((eq C c1 (CHead e1 (Bind
75 Abbr) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2 (Bind Abbr) v)))
76 (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (b: B).(\lambda (_: (not (eq B
77 b Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead c1
78 (Bind Void) u1) (CHead e1 (Bind Abbr) v))).(let H5 \def (eq_ind C (CHead c1
79 (Bind Void) u1) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False
80 | (CHead _ k _) \Rightarrow (match k with [(Bind b0) \Rightarrow (match b0
81 with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow
82 True]) | (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H4) in
83 (False_ind (ex2 C (\lambda (e2: C).(eq C (CHead c3 (Bind b) u2) (CHead e2
84 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2))) H5))))))))))) (\lambda
85 (c1: C).(\lambda (c3: C).(\lambda (_: (csubt g c1 c3)).(\lambda (_: (((eq C
86 c1 (CHead e1 (Bind Abbr) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2
87 (Bind Abbr) v))) (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (u:
88 T).(\lambda (t: T).(\lambda (_: (ty3 g c1 u t)).(\lambda (_: (ty3 g c3 u
89 t)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abbr)
90 v))).(let H6 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match
91 ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k
92 with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow False | Abst
93 \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])]))
94 I (CHead e1 (Bind Abbr) v) H5) in (False_ind (ex2 C (\lambda (e2: C).(eq C
95 (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csubt g
96 e1 e2))) H6))))))))))) y c2 H0))) H))))).
99 \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csubt g
100 (CHead e1 (Bind Abst) v1) c2) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead
101 e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda
102 (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
103 C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g
104 e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))))
106 \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v1: T).(\lambda
107 (H: (csubt g (CHead e1 (Bind Abst) v1) c2)).(insert_eq C (CHead e1 (Bind
108 Abst) v1) (\lambda (c: C).(csubt g c c2)) (\lambda (_: C).(or (ex2 C (\lambda
109 (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1
110 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
111 Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_:
112 C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3
113 g e2 v2 v1)))))) (\lambda (y: C).(\lambda (H0: (csubt g y c2)).(csubt_ind g
114 (\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind Abst) v1)) \to (or
115 (ex2 C (\lambda (e2: C).(eq C c0 (CHead e2 (Bind Abst) v1))) (\lambda (e2:
116 C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c0
117 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1
118 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
119 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) (\lambda (n: nat).(\lambda (H1:
120 (eq C (CSort n) (CHead e1 (Bind Abst) v1))).(let H2 \def (eq_ind C (CSort n)
121 (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow True | (CHead _ _ _)
122 \Rightarrow False])) I (CHead e1 (Bind Abst) v1) H1) in (False_ind (or (ex2 C
123 (\lambda (e2: C).(eq C (CSort n) (CHead e2 (Bind Abst) v1))) (\lambda (e2:
124 C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
125 (CSort n) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
126 T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1)))
127 (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1))))) H2)))) (\lambda (c1:
128 C).(\lambda (c3: C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C c1
129 (CHead e1 (Bind Abst) v1)) \to (or (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2
130 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2:
131 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
132 C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g
133 e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
134 v1)))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
135 (CHead e1 (Bind Abst) v1))).(let H4 \def (f_equal C C (\lambda (e: C).(match
136 e with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k
137 u) (CHead e1 (Bind Abst) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
138 C).(match e with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
139 (CHead c1 k u) (CHead e1 (Bind Abst) v1) H3) in ((let H6 \def (f_equal C T
140 (\lambda (e: C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t)
141 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind Abst) v1) H3) in (\lambda
142 (H7: (eq K k (Bind Abst))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v1
143 (\lambda (t: T).(or (ex2 C (\lambda (e2: C).(eq C (CHead c3 k t) (CHead e2
144 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2:
145 C).(\lambda (v2: T).(eq C (CHead c3 k t) (CHead e2 (Bind Abbr) v2))))
146 (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda
147 (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
148 v1)))))) (eq_ind_r K (Bind Abst) (\lambda (k0: K).(or (ex2 C (\lambda (e2:
149 C).(eq C (CHead c3 k0 v1) (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt
150 g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k0
151 v1) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1
152 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
153 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))) (let H9 \def (eq_ind C c1 (\lambda
154 (c: C).((eq C c (CHead e1 (Bind Abst) v1)) \to (or (ex2 C (\lambda (e2:
155 C).(eq C c3 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2)))
156 (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind Abbr)
157 v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_:
158 C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3
159 g e2 v2 v1))))))) H2 e1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c:
160 C).(csubt g c c3)) H1 e1 H8) in (or_introl (ex2 C (\lambda (e2: C).(eq C
161 (CHead c3 (Bind Abst) v1) (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt
162 g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind
163 Abst) v1) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
164 T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1)))
165 (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))) (ex_intro2 C (\lambda
166 (e2: C).(eq C (CHead c3 (Bind Abst) v1) (CHead e2 (Bind Abst) v1))) (\lambda
167 (e2: C).(csubt g e1 e2)) c3 (refl_equal C (CHead c3 (Bind Abst) v1)) H10))))
168 k H7) u H6)))) H5)) H4))))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda
169 (_: (csubt g c1 c3)).(\lambda (_: (((eq C c1 (CHead e1 (Bind Abst) v1)) \to
170 (or (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2 (Bind Abst) v1))) (\lambda
171 (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
172 c3 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1
173 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
174 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))).(\lambda (b: B).(\lambda (_: (not
175 (eq B b Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H4: (eq C (CHead
176 c1 (Bind Void) u1) (CHead e1 (Bind Abst) v1))).(let H5 \def (eq_ind C (CHead
177 c1 (Bind Void) u1) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow
178 False | (CHead _ k _) \Rightarrow (match k with [(Bind b0) \Rightarrow (match
179 b0 with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow
180 True]) | (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abst) v1) H4) in
181 (False_ind (or (ex2 C (\lambda (e2: C).(eq C (CHead c3 (Bind b) u2) (CHead e2
182 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2:
183 C).(\lambda (v2: T).(eq C (CHead c3 (Bind b) u2) (CHead e2 (Bind Abbr) v2))))
184 (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda
185 (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
186 v1))))) H5))))))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H1: (csubt
187 g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1 (Bind Abst) v1)) \to (or (ex2 C
188 (\lambda (e2: C).(eq C c3 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt
189 g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2
190 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2)))
191 (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda
192 (v2: T).(ty3 g e2 v2 v1)))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3:
193 (ty3 g c1 u t)).(\lambda (H4: (ty3 g c3 u t)).(\lambda (H5: (eq C (CHead c1
194 (Bind Abst) t) (CHead e1 (Bind Abst) v1))).(let H6 \def (f_equal C C (\lambda
195 (e: C).(match e with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow
196 c])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1) H5) in ((let H7 \def
197 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow t | (CHead
198 _ _ t0) \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1)
199 H5) in (\lambda (H8: (eq C c1 e1)).(let H9 \def (eq_ind T t (\lambda (t0:
200 T).(ty3 g c3 u t0)) H4 v1 H7) in (let H10 \def (eq_ind T t (\lambda (t0:
201 T).(ty3 g c1 u t0)) H3 v1 H7) in (let H11 \def (eq_ind C c1 (\lambda (c:
202 C).(ty3 g c u v1)) H10 e1 H8) in (let H12 \def (eq_ind C c1 (\lambda (c:
203 C).((eq C c (CHead e1 (Bind Abst) v1)) \to (or (ex2 C (\lambda (e2: C).(eq C
204 c3 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T
205 (\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind Abbr) v2))))
206 (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda
207 (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
208 v1))))))) H2 e1 H8) in (let H13 \def (eq_ind C c1 (\lambda (c: C).(csubt g c
209 c3)) H1 e1 H8) in (or_intror (ex2 C (\lambda (e2: C).(eq C (CHead c3 (Bind
210 Abbr) u) (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2)))
211 (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind Abbr) u)
212 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1
213 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
214 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))) (ex4_2_intro C T (\lambda (e2:
215 C).(\lambda (v2: T).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr)
216 v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_:
217 C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3
218 g e2 v2 v1))) c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H13 H11
219 H9))))))))) H6))))))))))) y c2 H0))) H))))).
221 lemma csubt_gen_flat:
222 \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).(\forall
223 (f: F).((csubt g (CHead e1 (Flat f) v) c2) \to (ex2 C (\lambda (e2: C).(eq C
224 c2 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2))))))))
226 \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda
227 (f: F).(\lambda (H: (csubt g (CHead e1 (Flat f) v) c2)).(insert_eq C (CHead
228 e1 (Flat f) v) (\lambda (c: C).(csubt g c c2)) (\lambda (_: C).(ex2 C
229 (\lambda (e2: C).(eq C c2 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g
230 e1 e2)))) (\lambda (y: C).(\lambda (H0: (csubt g y c2)).(csubt_ind g (\lambda
231 (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Flat f) v)) \to (ex2 C (\lambda
232 (e2: C).(eq C c0 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1
233 e2)))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead e1 (Flat f)
234 v))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee with [(CSort
235 _) \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Flat f)
236 v) H1) in (False_ind (ex2 C (\lambda (e2: C).(eq C (CSort n) (CHead e2 (Flat
237 f) v))) (\lambda (e2: C).(csubt g e1 e2))) H2)))) (\lambda (c1: C).(\lambda
238 (c3: C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1
239 (Flat f) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2 (Flat f) v)))
240 (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (k: K).(\lambda (u:
241 T).(\lambda (H3: (eq C (CHead c1 k u) (CHead e1 (Flat f) v))).(let H4 \def
242 (f_equal C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow c1 | (CHead
243 c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1 (Flat f) v) H3) in ((let H5
244 \def (f_equal C K (\lambda (e: C).(match e with [(CSort _) \Rightarrow k |
245 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Flat f) v) H3) in
246 ((let H6 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
247 \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead e1 (Flat
248 f) v) H3) in (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c1
249 e1)).(eq_ind_r T v (\lambda (t: T).(ex2 C (\lambda (e2: C).(eq C (CHead c3 k
250 t) (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2)))) (eq_ind_r K
251 (Flat f) (\lambda (k0: K).(ex2 C (\lambda (e2: C).(eq C (CHead c3 k0 v)
252 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2)))) (let H9 \def
253 (eq_ind C c1 (\lambda (c: C).((eq C c (CHead e1 (Flat f) v)) \to (ex2 C
254 (\lambda (e2: C).(eq C c3 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g
255 e1 e2))))) H2 e1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c: C).(csubt g c
256 c3)) H1 e1 H8) in (ex_intro2 C (\lambda (e2: C).(eq C (CHead c3 (Flat f) v)
257 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2)) c3 (refl_equal C
258 (CHead c3 (Flat f) v)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
259 C).(\lambda (c3: C).(\lambda (_: (csubt g c1 c3)).(\lambda (_: (((eq C c1
260 (CHead e1 (Flat f) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2 (Flat
261 f) v))) (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (b: B).(\lambda (_:
262 (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H4: (eq C
263 (CHead c1 (Bind Void) u1) (CHead e1 (Flat f) v))).(let H5 \def (eq_ind C
264 (CHead c1 (Bind Void) u1) (\lambda (ee: C).(match ee with [(CSort _)
265 \Rightarrow False | (CHead _ k _) \Rightarrow (match k with [(Bind _)
266 \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e1 (Flat f) v)
267 H4) in (False_ind (ex2 C (\lambda (e2: C).(eq C (CHead c3 (Bind b) u2) (CHead
268 e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2))) H5))))))))))) (\lambda
269 (c1: C).(\lambda (c3: C).(\lambda (_: (csubt g c1 c3)).(\lambda (_: (((eq C
270 c1 (CHead e1 (Flat f) v)) \to (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2
271 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2)))))).(\lambda (u: T).(\lambda
272 (t: T).(\lambda (_: (ty3 g c1 u t)).(\lambda (_: (ty3 g c3 u t)).(\lambda
273 (H5: (eq C (CHead c1 (Bind Abst) t) (CHead e1 (Flat f) v))).(let H6 \def
274 (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee with [(CSort _)
275 \Rightarrow False | (CHead _ k _) \Rightarrow (match k with [(Bind _)
276 \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e1 (Flat f) v)
277 H5) in (False_ind (ex2 C (\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) u)
278 (CHead e2 (Flat f) v))) (\lambda (e2: C).(csubt g e1 e2))) H6))))))))))) y c2
281 lemma csubt_gen_bind:
282 \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
283 (v1: T).((csubt g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
284 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
285 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))))))))))
287 \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
288 (v1: T).(\lambda (H: (csubt g (CHead e1 (Bind b1) v1) c2)).(insert_eq C
289 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csubt g c c2)) (\lambda (_:
290 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
291 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
292 T).(csubt g e1 e2)))))) (\lambda (y: C).(\lambda (H0: (csubt g y
293 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind
294 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
295 T).(eq C c0 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
296 C).(\lambda (_: T).(csubt g e1 e2)))))))) (\lambda (n: nat).(\lambda (H1: (eq
297 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
298 (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow True | (CHead _ _ _)
299 \Rightarrow False])) I (CHead e1 (Bind b1) v1) H1) in (False_ind (ex2_3 B C T
300 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CSort n) (CHead e2
301 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g
302 e1 e2))))) H2)))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H1: (csubt g c1
303 c3)).(\lambda (H2: (((eq C c1 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T
304 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind
305 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1
306 e2)))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
307 (CHead e1 (Bind b1) v1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
308 with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k
309 u) (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
310 C).(match e with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
311 (CHead c1 k u) (CHead e1 (Bind b1) v1) H3) in ((let H6 \def (f_equal C T
312 (\lambda (e: C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t)
313 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7:
314 (eq K k (Bind b1))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v1 (\lambda (t:
315 T).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
316 (CHead c3 k t) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
317 C).(\lambda (_: T).(csubt g e1 e2)))))) (eq_ind_r K (Bind b1) (\lambda (k0:
318 K).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
319 (CHead c3 k0 v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
320 C).(\lambda (_: T).(csubt g e1 e2)))))) (let H9 \def (eq_ind C c1 (\lambda
321 (c: C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
322 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2)))))
323 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))))))) H2 e1
324 H8) in (let H10 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c3)) H1 e1 H8)
325 in (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq
326 C (CHead c3 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_:
327 B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2)))) b1 c3 v1 (refl_equal C
328 (CHead c3 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
329 C).(\lambda (c3: C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C c1
330 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
331 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
332 B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2)))))))).(\lambda (b:
333 B).(\lambda (_: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
334 T).(\lambda (H4: (eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1)
335 v1))).(let H5 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
336 \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind Void) u1)
337 (CHead e1 (Bind b1) v1) H4) in ((let H6 \def (f_equal C B (\lambda (e:
338 C).(match e with [(CSort _) \Rightarrow Void | (CHead _ k _) \Rightarrow
339 (match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Void])]))
340 (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1) v1) H4) in ((let H7 \def
341 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u1 | (CHead
342 _ _ t) \Rightarrow t])) (CHead c1 (Bind Void) u1) (CHead e1 (Bind b1) v1) H4)
343 in (\lambda (H8: (eq B Void b1)).(\lambda (H9: (eq C c1 e1)).(let H10 \def
344 (eq_ind C c1 (\lambda (c: C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C
345 T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind
346 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1
347 e2))))))) H2 e1 H9) in (let H11 \def (eq_ind C c1 (\lambda (c: C).(csubt g c
348 c3)) H1 e1 H9) in (let H12 \def (eq_ind_r B b1 (\lambda (b0: B).((eq C e1
349 (CHead e1 (Bind b0) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
350 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
351 B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))))))) H10 Void H8) in
352 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
353 (CHead c3 (Bind b) u2) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
354 (e2: C).(\lambda (_: T).(csubt g e1 e2)))) b c3 u2 (refl_equal C (CHead c3
355 (Bind b) u2)) H11))))))) H6)) H5))))))))))) (\lambda (c1: C).(\lambda (c3:
356 C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1 (Bind
357 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
358 T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
359 C).(\lambda (_: T).(csubt g e1 e2)))))))).(\lambda (u: T).(\lambda (t:
360 T).(\lambda (H3: (ty3 g c1 u t)).(\lambda (H4: (ty3 g c3 u t)).(\lambda (H5:
361 (eq C (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1))).(let H6 \def
362 (f_equal C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow c1 | (CHead
363 c _ _) \Rightarrow c])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5)
364 in ((let H7 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
365 \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with [(Bind b)
366 \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead c1 (Bind Abst) t)
367 (CHead e1 (Bind b1) v1) H5) in ((let H8 \def (f_equal C T (\lambda (e:
368 C).(match e with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0]))
369 (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in (\lambda (H9: (eq B
370 Abst b1)).(\lambda (H10: (eq C c1 e1)).(let H11 \def (eq_ind T t (\lambda
371 (t0: T).(ty3 g c3 u t0)) H4 v1 H8) in (let H12 \def (eq_ind T t (\lambda (t0:
372 T).(ty3 g c1 u t0)) H3 v1 H8) in (let H13 \def (eq_ind C c1 (\lambda (c:
373 C).(ty3 g c u v1)) H12 e1 H10) in (let H14 \def (eq_ind C c1 (\lambda (c:
374 C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
375 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2)))))
376 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))))))) H2 e1
377 H10) in (let H15 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c3)) H1 e1 H10)
378 in (let H16 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1 (CHead e1 (Bind b)
379 v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq
380 C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda
381 (_: T).(csubt g e1 e2))))))) H14 Abst H9) in (ex2_3_intro B C T (\lambda (b2:
382 B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind Abbr) u) (CHead e2
383 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g
384 e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H15))))))))))
385 H7)) H6))))))))))) y c2 H0))) H)))))).