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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/arity/props".
19 include "arity/fwd.ma".
22 \forall (g: G).(\forall (n: nat).(\forall (k: nat).(ex_2 C T (\lambda (c:
23 C).(\lambda (t: T).(arity g c t (ASort k n)))))))
25 \lambda (g: G).(\lambda (n: nat).(\lambda (k: nat).(nat_ind (\lambda (n0:
26 nat).(ex_2 C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort n0 n))))))
27 (ex_2_intro C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort O n))))
28 (CSort O) (TSort n) (arity_sort g (CSort O) n)) (\lambda (n0: nat).(\lambda
29 (H: (ex_2 C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort n0
30 n)))))).(let H0 \def H in (ex_2_ind C T (\lambda (c: C).(\lambda (t:
31 T).(arity g c t (ASort n0 n)))) (ex_2 C T (\lambda (c: C).(\lambda (t:
32 T).(arity g c t (ASort (S n0) n))))) (\lambda (x0: C).(\lambda (x1:
33 T).(\lambda (H1: (arity g x0 x1 (ASort n0 n))).(ex_2_intro C T (\lambda (c:
34 C).(\lambda (t: T).(arity g c t (ASort (S n0) n)))) (CHead x0 (Bind Abst) x1)
35 (TLRef O) (arity_abst g (CHead x0 (Bind Abst) x1) x0 x1 O (getl_refl Abst x0
36 x1) (ASort (S n0) n) H1))))) H0)))) k))).
39 \forall (g: G).(\forall (c2: C).(\forall (t: T).(\forall (a: A).((arity g c2
40 t a) \to (\forall (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1
41 c2) \to (arity g c1 (lift h d t) a)))))))))
43 \lambda (g: G).(\lambda (c2: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
44 (arity g c2 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0:
45 A).(\forall (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to
46 (arity g c1 (lift h d t0) a0)))))))) (\lambda (c: C).(\lambda (n:
47 nat).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (_: (drop
48 h d c1 c)).(eq_ind_r T (TSort n) (\lambda (t0: T).(arity g c1 t0 (ASort O
49 n))) (arity_sort g c1 n) (lift h d (TSort n)) (lift_sort n h d))))))))
50 (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
51 (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H1:
52 (arity g d u a0)).(\lambda (H2: ((\forall (c1: C).(\forall (h: nat).(\forall
53 (d0: nat).((drop h d0 c1 d) \to (arity g c1 (lift h d0 u) a0))))))).(\lambda
54 (c1: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda (H3: (drop h d0 c1
55 c)).(lt_le_e i d0 (arity g c1 (lift h d0 (TLRef i)) a0) (\lambda (H4: (lt i
56 d0)).(eq_ind_r T (TLRef i) (\lambda (t0: T).(arity g c1 t0 a0)) (let H5 \def
57 (drop_getl_trans_le i d0 (le_S_n i d0 (le_S (S i) d0 H4)) c1 c h H3 (CHead d
58 (Bind Abbr) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i
59 O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 i) e0 e1)))
60 (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (arity
61 g c1 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop i O
62 c1 x0)).(\lambda (H7: (drop h (minus d0 i) x0 x1)).(\lambda (H8: (clear x1
63 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind nat (minus d0 i) (\lambda (n:
64 nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let
65 H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) H9 Abbr d u H8) in (ex2_ind C
66 (\lambda (c3: C).(clear x0 (CHead c3 (Bind Abbr) (lift h (minus d0 (S i))
67 u)))) (\lambda (c3: C).(drop h (minus d0 (S i)) c3 d)) (arity g c1 (TLRef i)
68 a0) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h
69 (minus d0 (S i)) u)))).(\lambda (H12: (drop h (minus d0 (S i)) x
70 d)).(arity_abbr g c1 x (lift h (minus d0 (S i)) u) i (getl_intro i c1 (CHead
71 x (Bind Abbr) (lift h (minus d0 (S i)) u)) x0 H6 H11) a0 (H2 x h (minus d0 (S
72 i)) H12))))) H10)))))))) H5)) (lift h d0 (TLRef i)) (lift_lref_lt i h d0
73 H4))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus i h)) (\lambda (t0:
74 T).(arity g c1 t0 a0)) (arity_abbr g c1 d u (plus i h) (drop_getl_trans_ge i
75 c1 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) a0 H1) (lift h d0 (TLRef i))
76 (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (d:
77 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind
78 Abst) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u (asucc g
79 a0))).(\lambda (H2: ((\forall (c1: C).(\forall (h: nat).(\forall (d0:
80 nat).((drop h d0 c1 d) \to (arity g c1 (lift h d0 u) (asucc g
81 a0)))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda
82 (H3: (drop h d0 c1 c)).(lt_le_e i d0 (arity g c1 (lift h d0 (TLRef i)) a0)
83 (\lambda (H4: (lt i d0)).(eq_ind_r T (TLRef i) (\lambda (t0: T).(arity g c1
84 t0 a0)) (let H5 \def (drop_getl_trans_le i d0 (le_S_n i d0 (le_S (S i) d0
85 H4)) c1 c h H3 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0:
86 C).(\lambda (_: C).(drop i O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop
87 h (minus d0 i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d
88 (Bind Abst) u)))) (arity g c1 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1:
89 C).(\lambda (H6: (drop i O c1 x0)).(\lambda (H7: (drop h (minus d0 i) x0
90 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let H9 \def (eq_ind
91 nat (minus d0 i) (\lambda (n: nat).(drop h n x0 x1)) H7 (S (minus d0 (S i)))
92 (minus_x_Sy d0 i H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0 (S i))
93 H9 Abst d u H8) in (ex2_ind C (\lambda (c3: C).(clear x0 (CHead c3 (Bind
94 Abst) (lift h (minus d0 (S i)) u)))) (\lambda (c3: C).(drop h (minus d0 (S
95 i)) c3 d)) (arity g c1 (TLRef i) a0) (\lambda (x: C).(\lambda (H11: (clear x0
96 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u)))).(\lambda (H12: (drop h
97 (minus d0 (S i)) x d)).(arity_abst g c1 x (lift h (minus d0 (S i)) u) i
98 (getl_intro i c1 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u)) x0 H6 H11)
99 a0 (H2 x h (minus d0 (S i)) H12))))) H10)))))))) H5)) (lift h d0 (TLRef i))
100 (lift_lref_lt i h d0 H4))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus
101 i h)) (\lambda (t0: T).(arity g c1 t0 a0)) (arity_abst g c1 d u (plus i h)
102 (drop_getl_trans_ge i c1 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) a0 H1)
103 (lift h d0 (TLRef i)) (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (b:
104 B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda (u:
105 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall
106 (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1
107 (lift h d u) a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity
108 g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (c1: C).(\forall (h:
109 nat).(\forall (d: nat).((drop h d c1 (CHead c (Bind b) u)) \to (arity g c1
110 (lift h d t0) a2))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d:
111 nat).(\lambda (H5: (drop h d c1 c)).(eq_ind_r T (THead (Bind b) (lift h d u)
112 (lift h (s (Bind b) d) t0)) (\lambda (t1: T).(arity g c1 t1 a2)) (arity_bind
113 g b H0 c1 (lift h d u) a1 (H2 c1 h d H5) (lift h (s (Bind b) d) t0) a2 (H4
114 (CHead c1 (Bind b) (lift h d u)) h (s (Bind b) d) (drop_skip_bind h d c1 c H5
115 b u))) (lift h d (THead (Bind b) u t0)) (lift_head (Bind b) u t0 h
116 d))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda
117 (_: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c1: C).(\forall (h:
118 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d u) (asucc g
119 a1)))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c
120 (Bind Abst) u) t0 a2)).(\lambda (H3: ((\forall (c1: C).(\forall (h:
121 nat).(\forall (d: nat).((drop h d c1 (CHead c (Bind Abst) u)) \to (arity g c1
122 (lift h d t0) a2))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d:
123 nat).(\lambda (H4: (drop h d c1 c)).(eq_ind_r T (THead (Bind Abst) (lift h d
124 u) (lift h (s (Bind Abst) d) t0)) (\lambda (t1: T).(arity g c1 t1 (AHead a1
125 a2))) (arity_head g c1 (lift h d u) a1 (H1 c1 h d H4) (lift h (s (Bind Abst)
126 d) t0) a2 (H3 (CHead c1 (Bind Abst) (lift h d u)) h (s (Bind Abst) d)
127 (drop_skip_bind h d c1 c H4 Abst u))) (lift h d (THead (Bind Abst) u t0))
128 (lift_head (Bind Abst) u t0 h d))))))))))))))) (\lambda (c: C).(\lambda (u:
129 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: ((\forall
130 (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1
131 (lift h d u) a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity
132 g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (c1: C).(\forall (h:
133 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d t0) (AHead
134 a1 a2)))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda
135 (H4: (drop h d c1 c)).(eq_ind_r T (THead (Flat Appl) (lift h d u) (lift h (s
136 (Flat Appl) d) t0)) (\lambda (t1: T).(arity g c1 t1 a2)) (arity_appl g c1
137 (lift h d u) a1 (H1 c1 h d H4) (lift h (s (Flat Appl) d) t0) a2 (H3 c1 h (s
138 (Flat Appl) d) H4)) (lift h d (THead (Flat Appl) u t0)) (lift_head (Flat
139 Appl) u t0 h d))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a0:
140 A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1: ((\forall (c1:
141 C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift
142 h d u) (asucc g a0)))))))).(\lambda (t0: T).(\lambda (_: (arity g c t0
143 a0)).(\lambda (H3: ((\forall (c1: C).(\forall (h: nat).(\forall (d:
144 nat).((drop h d c1 c) \to (arity g c1 (lift h d t0) a0))))))).(\lambda (c1:
145 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H4: (drop h d c1
146 c)).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d)
147 t0)) (\lambda (t1: T).(arity g c1 t1 a0)) (arity_cast g c1 (lift h d u) a0
148 (H1 c1 h d H4) (lift h (s (Flat Cast) d) t0) (H3 c1 h (s (Flat Cast) d) H4))
149 (lift h d (THead (Flat Cast) u t0)) (lift_head (Flat Cast) u t0 h
150 d)))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda
151 (_: (arity g c t0 a1)).(\lambda (H1: ((\forall (c1: C).(\forall (h:
152 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d t0)
153 a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c1:
154 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H3: (drop h d c1
155 c)).(arity_repl g c1 (lift h d t0) a1 (H1 c1 h d H3) a2 H2)))))))))))) c2 t a
159 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a1: A).((arity g c
160 t a1) \to (\forall (a2: A).((arity g c t a2) \to (leq g a1 a2)))))))
162 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a1: A).(\lambda (H:
163 (arity g c t a1)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a:
164 A).(\forall (a2: A).((arity g c0 t0 a2) \to (leq g a a2)))))) (\lambda (c0:
165 C).(\lambda (n: nat).(\lambda (a2: A).(\lambda (H0: (arity g c0 (TSort n)
166 a2)).(leq_sym g a2 (ASort O n) (arity_gen_sort g c0 n a2 H0)))))) (\lambda
167 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl
168 i c0 (CHead d (Bind Abbr) u))).(\lambda (a: A).(\lambda (_: (arity g d u
169 a)).(\lambda (H2: ((\forall (a2: A).((arity g d u a2) \to (leq g a
170 a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i) a2)).(let H4
171 \def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T (\lambda (d0:
172 C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0:
173 C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda (d0:
174 C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0:
175 C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2) (\lambda
176 (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind
177 Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
178 a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0
179 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))
180 (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0
181 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (arity g x0 x1 a2)).(let H8 \def
182 (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead
183 x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind
184 Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C
185 return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _)
186 \Rightarrow c1])) (CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1)
187 (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in
188 ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
189 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
190 d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr)
191 u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in (\lambda (H11: (eq C d x0)).(let
192 H12 \def (eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind Abbr)
193 t0))) H8 u H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity g x0
194 t0 a2)) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl i c0
195 (CHead c1 (Bind Abbr) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0
196 (\lambda (c1: C).(arity g c1 u a2)) H13 d H11) in (H2 a2 H15))))))) H9)))))))
197 H5)) (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0
198 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
199 (asucc g a2)))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0
200 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
201 (asucc g a2)))) (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6:
202 (getl i c0 (CHead x0 (Bind Abst) x1))).(\lambda (_: (arity g x0 x1 (asucc g
203 a2))).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i
204 c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i
205 H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind
206 Abbr) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with
207 [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return
208 (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
209 (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False |
210 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind
211 Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind Abst)
212 x1) H6)) in (False_ind (leq g a a2) H9))))))) H5)) H4)))))))))))) (\lambda
213 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl
214 i c0 (CHead d (Bind Abst) u))).(\lambda (a: A).(\lambda (_: (arity g d u
215 (asucc g a))).(\lambda (H2: ((\forall (a2: A).((arity g d u a2) \to (leq g
216 (asucc g a) a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i)
217 a2)).(let H4 \def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T
218 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0))))
219 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda
220 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda
221 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2)
222 (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead
223 d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
224 a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0
225 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))
226 (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0
227 (CHead x0 (Bind Abbr) x1))).(\lambda (_: (arity g x0 x1 a2)).(let H8 \def
228 (eq_ind C (CHead d (Bind Abst) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead
229 x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind
230 Abbr) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda
231 (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
232 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
233 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
234 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void
235 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abbr)
236 x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abbr) x1) H6))
237 in (False_ind (leq g a a2) H9))))))) H5)) (\lambda (H5: (ex2_2 C T (\lambda
238 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda
239 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2)))))).(ex2_2_ind C T
240 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0))))
241 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2)))) (leq g a a2)
242 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0 (CHead x0 (Bind
243 Abst) x1))).(\lambda (H7: (arity g x0 x1 (asucc g a2))).(let H8 \def (eq_ind
244 C (CHead d (Bind Abst) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead x0 (Bind
245 Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abst)
246 x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C return
247 (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow
248 c1])) (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead
249 d (Bind Abst) u) i H0 (CHead x0 (Bind Abst) x1) H6)) in ((let H10 \def
250 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
251 [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind
252 Abst) u) (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0
253 (CHead x0 (Bind Abst) x1) H6)) in (\lambda (H11: (eq C d x0)).(let H12 \def
254 (eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind Abst) t0))) H8 u
255 H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity g x0 t0 (asucc g
256 a2))) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl i c0
257 (CHead c1 (Bind Abst) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0
258 (\lambda (c1: C).(arity g c1 u (asucc g a2))) H13 d H11) in (asucc_inj g a a2
259 (H2 (asucc g a2) H15)))))))) H9))))))) H5)) H4)))))))))))) (\lambda (b:
260 B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c0: C).(\lambda (u:
261 T).(\lambda (a2: A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall
262 (a3: A).((arity g c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda
263 (a3: A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t0 a3)).(\lambda (H4:
264 ((\forall (a4: A).((arity g (CHead c0 (Bind b) u) t0 a4) \to (leq g a3
265 a4))))).(\lambda (a0: A).(\lambda (H5: (arity g c0 (THead (Bind b) u t0)
266 a0)).(let H6 \def (arity_gen_bind b H0 g c0 u t0 a0 H5) in (ex2_ind A
267 (\lambda (a4: A).(arity g c0 u a4)) (\lambda (_: A).(arity g (CHead c0 (Bind
268 b) u) t0 a0)) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g c0 u
269 x)).(\lambda (H8: (arity g (CHead c0 (Bind b) u) t0 a0)).(H4 a0 H8))))
270 H6))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2: A).(\lambda
271 (_: (arity g c0 u (asucc g a2))).(\lambda (H1: ((\forall (a3: A).((arity g c0
272 u a3) \to (leq g (asucc g a2) a3))))).(\lambda (t0: T).(\lambda (a3:
273 A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t0 a3)).(\lambda (H3:
274 ((\forall (a4: A).((arity g (CHead c0 (Bind Abst) u) t0 a4) \to (leq g a3
275 a4))))).(\lambda (a0: A).(\lambda (H4: (arity g c0 (THead (Bind Abst) u t0)
276 a0)).(let H5 \def (arity_gen_abst g c0 u t0 a0 H4) in (ex3_2_ind A A (\lambda
277 (a4: A).(\lambda (a5: A).(eq A a0 (AHead a4 a5)))) (\lambda (a4: A).(\lambda
278 (_: A).(arity g c0 u (asucc g a4)))) (\lambda (_: A).(\lambda (a5: A).(arity
279 g (CHead c0 (Bind Abst) u) t0 a5))) (leq g (AHead a2 a3) a0) (\lambda (x0:
280 A).(\lambda (x1: A).(\lambda (H6: (eq A a0 (AHead x0 x1))).(\lambda (H7:
281 (arity g c0 u (asucc g x0))).(\lambda (H8: (arity g (CHead c0 (Bind Abst) u)
282 t0 x1)).(eq_ind_r A (AHead x0 x1) (\lambda (a: A).(leq g (AHead a2 a3) a))
283 (leq_head g a2 x0 (asucc_inj g a2 x0 (H1 (asucc g x0) H7)) a3 x1 (H3 x1 H8))
284 a0 H6)))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2:
285 A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall (a3: A).((arity g
286 c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda (a3: A).(\lambda (_:
287 (arity g c0 t0 (AHead a2 a3))).(\lambda (H3: ((\forall (a4: A).((arity g c0
288 t0 a4) \to (leq g (AHead a2 a3) a4))))).(\lambda (a0: A).(\lambda (H4: (arity
289 g c0 (THead (Flat Appl) u t0) a0)).(let H5 \def (arity_gen_appl g c0 u t0 a0
290 H4) in (ex2_ind A (\lambda (a4: A).(arity g c0 u a4)) (\lambda (a4: A).(arity
291 g c0 t0 (AHead a4 a0))) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g
292 c0 u x)).(\lambda (H7: (arity g c0 t0 (AHead x a0))).(ahead_inj_snd g a2 a3 x
293 a0 (H3 (AHead x a0) H7))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u:
294 T).(\lambda (a: A).(\lambda (_: (arity g c0 u (asucc g a))).(\lambda (_:
295 ((\forall (a2: A).((arity g c0 u a2) \to (leq g (asucc g a) a2))))).(\lambda
296 (t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2:
297 A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4:
298 (arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u
299 t0 a2 H4) in (and_ind (arity g c0 u (asucc g a2)) (arity g c0 t0 a2) (leq g a
300 a2) (\lambda (_: (arity g c0 u (asucc g a2))).(\lambda (H7: (arity g c0 t0
301 a2)).(H3 a2 H7))) H5)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda
302 (a2: A).(\lambda (_: (arity g c0 t0 a2)).(\lambda (H1: ((\forall (a3:
303 A).((arity g c0 t0 a3) \to (leq g a2 a3))))).(\lambda (a3: A).(\lambda (H2:
304 (leq g a2 a3)).(\lambda (a0: A).(\lambda (H3: (arity g c0 t0 a0)).(leq_trans
305 g a3 a2 (leq_sym g a2 a3 H2) a0 (H1 a0 H3))))))))))) c t a1 H))))).
307 theorem arity_appls_cast:
308 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (vs:
309 TList).(\forall (a: A).((arity g c (THeads (Flat Appl) vs u) (asucc g a)) \to
310 ((arity g c (THeads (Flat Appl) vs t) a) \to (arity g c (THeads (Flat Appl)
311 vs (THead (Flat Cast) u t)) a))))))))
313 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (vs:
314 TList).(TList_ind (\lambda (t0: TList).(\forall (a: A).((arity g c (THeads
315 (Flat Appl) t0 u) (asucc g a)) \to ((arity g c (THeads (Flat Appl) t0 t) a)
316 \to (arity g c (THeads (Flat Appl) t0 (THead (Flat Cast) u t)) a)))))
317 (\lambda (a: A).(\lambda (H: (arity g c u (asucc g a))).(\lambda (H0: (arity
318 g c t a)).(arity_cast g c u a H t H0)))) (\lambda (t0: T).(\lambda (t1:
319 TList).(\lambda (H: ((\forall (a: A).((arity g c (THeads (Flat Appl) t1 u)
320 (asucc g a)) \to ((arity g c (THeads (Flat Appl) t1 t) a) \to (arity g c
321 (THeads (Flat Appl) t1 (THead (Flat Cast) u t)) a)))))).(\lambda (a:
322 A).(\lambda (H0: (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 u))
323 (asucc g a))).(\lambda (H1: (arity g c (THead (Flat Appl) t0 (THeads (Flat
324 Appl) t1 t)) a)).(let H2 \def (arity_gen_appl g c t0 (THeads (Flat Appl) t1
325 t) a H1) in (ex2_ind A (\lambda (a1: A).(arity g c t0 a1)) (\lambda (a1:
326 A).(arity g c (THeads (Flat Appl) t1 t) (AHead a1 a))) (arity g c (THead
327 (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Flat Cast) u t))) a) (\lambda
328 (x: A).(\lambda (H3: (arity g c t0 x)).(\lambda (H4: (arity g c (THeads (Flat
329 Appl) t1 t) (AHead x a))).(let H5 \def (arity_gen_appl g c t0 (THeads (Flat
330 Appl) t1 u) (asucc g a) H0) in (ex2_ind A (\lambda (a1: A).(arity g c t0 a1))
331 (\lambda (a1: A).(arity g c (THeads (Flat Appl) t1 u) (AHead a1 (asucc g
332 a)))) (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Flat
333 Cast) u t))) a) (\lambda (x0: A).(\lambda (H6: (arity g c t0 x0)).(\lambda
334 (H7: (arity g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g
335 a)))).(arity_appl g c t0 x H3 (THeads (Flat Appl) t1 (THead (Flat Cast) u t))
336 a (H (AHead x a) (arity_repl g c (THeads (Flat Appl) t1 u) (AHead x (asucc g
337 a)) (arity_repl g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g a)) H7
338 (AHead x (asucc g a)) (leq_head g x0 x (arity_mono g c t0 x0 H6 x H3) (asucc
339 g a) (asucc g a) (leq_refl g (asucc g a)))) (asucc g (AHead x a)) (leq_refl g
340 (asucc g (AHead x a)))) H4))))) H5))))) H2)))))))) vs))))).
342 theorem arity_appls_abbr:
343 \forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i:
344 nat).((getl i c (CHead d (Bind Abbr) v)) \to (\forall (vs: TList).(\forall
345 (a: A).((arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a) \to (arity g c
346 (THeads (Flat Appl) vs (TLRef i)) a)))))))))
348 \lambda (g: G).(\lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i:
349 nat).(\lambda (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (vs:
350 TList).(TList_ind (\lambda (t: TList).(\forall (a: A).((arity g c (THeads
351 (Flat Appl) t (lift (S i) O v)) a) \to (arity g c (THeads (Flat Appl) t
352 (TLRef i)) a)))) (\lambda (a: A).(\lambda (H0: (arity g c (lift (S i) O v)
353 a)).(arity_abbr g c d v i H a (arity_gen_lift g c v a (S i) O H0 d (getl_drop
354 Abbr c d v i H))))) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0:
355 ((\forall (a: A).((arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) a) \to
356 (arity g c (THeads (Flat Appl) t0 (TLRef i)) a))))).(\lambda (a: A).(\lambda
357 (H1: (arity g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O
358 v))) a)).(let H2 \def (arity_gen_appl g c t (THeads (Flat Appl) t0 (lift (S
359 i) O v)) a H1) in (ex2_ind A (\lambda (a1: A).(arity g c t a1)) (\lambda (a1:
360 A).(arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) (AHead a1 a))) (arity
361 g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) a) (\lambda (x:
362 A).(\lambda (H3: (arity g c t x)).(\lambda (H4: (arity g c (THeads (Flat
363 Appl) t0 (lift (S i) O v)) (AHead x a))).(arity_appl g c t x H3 (THeads (Flat
364 Appl) t0 (TLRef i)) a (H0 (AHead x a) H4))))) H2))))))) vs))))))).
366 theorem arity_appls_bind:
367 \forall (g: G).(\forall (b: B).((not (eq B b Abst)) \to (\forall (c:
368 C).(\forall (v: T).(\forall (a1: A).((arity g c v a1) \to (\forall (t:
369 T).(\forall (vs: TList).(\forall (a2: A).((arity g (CHead c (Bind b) v)
370 (THeads (Flat Appl) (lifts (S O) O vs) t) a2) \to (arity g c (THeads (Flat
371 Appl) vs (THead (Bind b) v t)) a2)))))))))))
373 \lambda (g: G).(\lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda
374 (c: C).(\lambda (v: T).(\lambda (a1: A).(\lambda (H0: (arity g c v
375 a1)).(\lambda (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0:
376 TList).(\forall (a2: A).((arity g (CHead c (Bind b) v) (THeads (Flat Appl)
377 (lifts (S O) O t0) t) a2) \to (arity g c (THeads (Flat Appl) t0 (THead (Bind
378 b) v t)) a2)))) (\lambda (a2: A).(\lambda (H1: (arity g (CHead c (Bind b) v)
379 t a2)).(arity_bind g b H c v a1 H0 t a2 H1))) (\lambda (t0: T).(\lambda (t1:
380 TList).(\lambda (H1: ((\forall (a2: A).((arity g (CHead c (Bind b) v) (THeads
381 (Flat Appl) (lifts (S O) O t1) t) a2) \to (arity g c (THeads (Flat Appl) t1
382 (THead (Bind b) v t)) a2))))).(\lambda (a2: A).(\lambda (H2: (arity g (CHead
383 c (Bind b) v) (THead (Flat Appl) (lift (S O) O t0) (THeads (Flat Appl) (lifts
384 (S O) O t1) t)) a2)).(let H3 \def (arity_gen_appl g (CHead c (Bind b) v)
385 (lift (S O) O t0) (THeads (Flat Appl) (lifts (S O) O t1) t) a2 H2) in
386 (ex2_ind A (\lambda (a3: A).(arity g (CHead c (Bind b) v) (lift (S O) O t0)
387 a3)) (\lambda (a3: A).(arity g (CHead c (Bind b) v) (THeads (Flat Appl)
388 (lifts (S O) O t1) t) (AHead a3 a2))) (arity g c (THead (Flat Appl) t0
389 (THeads (Flat Appl) t1 (THead (Bind b) v t))) a2) (\lambda (x: A).(\lambda
390 (H4: (arity g (CHead c (Bind b) v) (lift (S O) O t0) x)).(\lambda (H5: (arity
391 g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O t1) t) (AHead x
392 a2))).(arity_appl g c t0 x (arity_gen_lift g (CHead c (Bind b) v) t0 x (S O)
393 O H4 c (drop_drop (Bind b) O c c (drop_refl c) v)) (THeads (Flat Appl) t1
394 (THead (Bind b) v t)) a2 (H1 (AHead x a2) H5))))) H3))))))) vs))))))))).