]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1/arity/props.ma
refactoring of \lambda\delta version 1 in matita
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / arity / props.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "Basic-1/arity/fwd.ma".
18
19 theorem node_inh:
20  \forall (g: G).(\forall (n: nat).(\forall (k: nat).(ex_2 C T (\lambda (c: 
21 C).(\lambda (t: T).(arity g c t (ASort k n)))))))
22 \def
23  \lambda (g: G).(\lambda (n: nat).(\lambda (k: nat).(nat_ind (\lambda (n0: 
24 nat).(ex_2 C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort n0 n)))))) 
25 (ex_2_intro C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort O n)))) 
26 (CSort O) (TSort n) (arity_sort g (CSort O) n)) (\lambda (n0: nat).(\lambda 
27 (H: (ex_2 C T (\lambda (c: C).(\lambda (t: T).(arity g c t (ASort n0 
28 n)))))).(let H0 \def H in (ex_2_ind C T (\lambda (c: C).(\lambda (t: 
29 T).(arity g c t (ASort n0 n)))) (ex_2 C T (\lambda (c: C).(\lambda (t: 
30 T).(arity g c t (ASort (S n0) n))))) (\lambda (x0: C).(\lambda (x1: 
31 T).(\lambda (H1: (arity g x0 x1 (ASort n0 n))).(ex_2_intro C T (\lambda (c: 
32 C).(\lambda (t: T).(arity g c t (ASort (S n0) n)))) (CHead x0 (Bind Abst) x1) 
33 (TLRef O) (arity_abst g (CHead x0 (Bind Abst) x1) x0 x1 O (getl_refl Abst x0 
34 x1) (ASort (S n0) n) H1))))) H0)))) k))).
35 (* COMMENTS
36 Initial nodes: 253
37 END *)
38
39 theorem arity_lift:
40  \forall (g: G).(\forall (c2: C).(\forall (t: T).(\forall (a: A).((arity g c2 
41 t a) \to (\forall (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 
42 c2) \to (arity g c1 (lift h d t) a)))))))))
43 \def
44  \lambda (g: G).(\lambda (c2: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H: 
45 (arity g c2 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0: 
46 A).(\forall (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to 
47 (arity g c1 (lift h d t0) a0)))))))) (\lambda (c: C).(\lambda (n: 
48 nat).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (_: (drop 
49 h d c1 c)).(eq_ind_r T (TSort n) (\lambda (t0: T).(arity g c1 t0 (ASort O 
50 n))) (arity_sort g c1 n) (lift h d (TSort n)) (lift_sort n h d)))))))) 
51 (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
52 (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (H1: 
53 (arity g d u a0)).(\lambda (H2: ((\forall (c1: C).(\forall (h: nat).(\forall 
54 (d0: nat).((drop h d0 c1 d) \to (arity g c1 (lift h d0 u) a0))))))).(\lambda 
55 (c1: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda (H3: (drop h d0 c1 
56 c)).(lt_le_e i d0 (arity g c1 (lift h d0 (TLRef i)) a0) (\lambda (H4: (lt i 
57 d0)).(eq_ind_r T (TLRef i) (\lambda (t0: T).(arity g c1 t0 a0)) (let H5 \def 
58 (drop_getl_trans_le i d0 (le_S_n i d0 (le_S (S i) d0 H4)) c1 c h H3 (CHead d 
59 (Bind Abbr) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i 
60 O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 i) e0 e1))) 
61 (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (arity 
62 g c1 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop i O 
63 c1 x0)).(\lambda (H7: (drop h (minus d0 i) x0 x1)).(\lambda (H8: (clear x1 
64 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind nat (minus d0 i) (\lambda (n: 
65 nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let 
66 H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) H9 Abbr d u H8) in (ex2_ind C 
67 (\lambda (c3: C).(clear x0 (CHead c3 (Bind Abbr) (lift h (minus d0 (S i)) 
68 u)))) (\lambda (c3: C).(drop h (minus d0 (S i)) c3 d)) (arity g c1 (TLRef i) 
69 a0) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h 
70 (minus d0 (S i)) u)))).(\lambda (H12: (drop h (minus d0 (S i)) x 
71 d)).(arity_abbr g c1 x (lift h (minus d0 (S i)) u) i (getl_intro i c1 (CHead 
72 x (Bind Abbr) (lift h (minus d0 (S i)) u)) x0 H6 H11) a0 (H2 x h (minus d0 (S 
73 i)) H12))))) H10)))))))) H5)) (lift h d0 (TLRef i)) (lift_lref_lt i h d0 
74 H4))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus i h)) (\lambda (t0: 
75 T).(arity g c1 t0 a0)) (arity_abbr g c1 d u (plus i h) (drop_getl_trans_ge i 
76 c1 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) a0 H1) (lift h d0 (TLRef i)) 
77 (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (d: 
78 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind 
79 Abst) u))).(\lambda (a0: A).(\lambda (H1: (arity g d u (asucc g 
80 a0))).(\lambda (H2: ((\forall (c1: C).(\forall (h: nat).(\forall (d0: 
81 nat).((drop h d0 c1 d) \to (arity g c1 (lift h d0 u) (asucc g 
82 a0)))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda 
83 (H3: (drop h d0 c1 c)).(lt_le_e i d0 (arity g c1 (lift h d0 (TLRef i)) a0) 
84 (\lambda (H4: (lt i d0)).(eq_ind_r T (TLRef i) (\lambda (t0: T).(arity g c1 
85 t0 a0)) (let H5 \def (drop_getl_trans_le i d0 (le_S_n i d0 (le_S (S i) d0 
86 H4)) c1 c h H3 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0: 
87 C).(\lambda (_: C).(drop i O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop 
88 h (minus d0 i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d 
89 (Bind Abst) u)))) (arity g c1 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: 
90 C).(\lambda (H6: (drop i O c1 x0)).(\lambda (H7: (drop h (minus d0 i) x0 
91 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let H9 \def (eq_ind 
92 nat (minus d0 i) (\lambda (n: nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) 
93 (minus_x_Sy d0 i H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) 
94 H9 Abst d u H8) in (ex2_ind C (\lambda (c3: C).(clear x0 (CHead c3 (Bind 
95 Abst) (lift h (minus d0 (S i)) u)))) (\lambda (c3: C).(drop h (minus d0 (S 
96 i)) c3 d)) (arity g c1 (TLRef i) a0) (\lambda (x: C).(\lambda (H11: (clear x0 
97 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u)))).(\lambda (H12: (drop h 
98 (minus d0 (S i)) x d)).(arity_abst g c1 x (lift h (minus d0 (S i)) u) i 
99 (getl_intro i c1 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u)) x0 H6 H11) 
100 a0 (H2 x h (minus d0 (S i)) H12))))) H10)))))))) H5)) (lift h d0 (TLRef i)) 
101 (lift_lref_lt i h d0 H4))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus 
102 i h)) (\lambda (t0: T).(arity g c1 t0 a0)) (arity_abst g c1 d u (plus i h) 
103 (drop_getl_trans_ge i c1 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) a0 H1) 
104 (lift h d0 (TLRef i)) (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (b: 
105 B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda (u: 
106 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall 
107 (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 
108 (lift h d u) a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity 
109 g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (c1: C).(\forall (h: 
110 nat).(\forall (d: nat).((drop h d c1 (CHead c (Bind b) u)) \to (arity g c1 
111 (lift h d t0) a2))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: 
112 nat).(\lambda (H5: (drop h d c1 c)).(eq_ind_r T (THead (Bind b) (lift h d u) 
113 (lift h (s (Bind b) d) t0)) (\lambda (t1: T).(arity g c1 t1 a2)) (arity_bind 
114 g b H0 c1 (lift h d u) a1 (H2 c1 h d H5) (lift h (s (Bind b) d) t0) a2 (H4 
115 (CHead c1 (Bind b) (lift h d u)) h (s (Bind b) d) (drop_skip_bind h d c1 c H5 
116 b u))) (lift h d (THead (Bind b) u t0)) (lift_head (Bind b) u t0 h 
117 d))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda 
118 (_: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c1: C).(\forall (h: 
119 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d u) (asucc g 
120 a1)))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c 
121 (Bind Abst) u) t0 a2)).(\lambda (H3: ((\forall (c1: C).(\forall (h: 
122 nat).(\forall (d: nat).((drop h d c1 (CHead c (Bind Abst) u)) \to (arity g c1 
123 (lift h d t0) a2))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: 
124 nat).(\lambda (H4: (drop h d c1 c)).(eq_ind_r T (THead (Bind Abst) (lift h d 
125 u) (lift h (s (Bind Abst) d) t0)) (\lambda (t1: T).(arity g c1 t1 (AHead a1 
126 a2))) (arity_head g c1 (lift h d u) a1 (H1 c1 h d H4) (lift h (s (Bind Abst) 
127 d) t0) a2 (H3 (CHead c1 (Bind Abst) (lift h d u)) h (s (Bind Abst) d) 
128 (drop_skip_bind h d c1 c H4 Abst u))) (lift h d (THead (Bind Abst) u t0)) 
129 (lift_head (Bind Abst) u t0 h d))))))))))))))) (\lambda (c: C).(\lambda (u: 
130 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: ((\forall 
131 (c1: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 
132 (lift h d u) a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity 
133 g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (c1: C).(\forall (h: 
134 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d t0) (AHead 
135 a1 a2)))))))).(\lambda (c1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda 
136 (H4: (drop h d c1 c)).(eq_ind_r T (THead (Flat Appl) (lift h d u) (lift h (s 
137 (Flat Appl) d) t0)) (\lambda (t1: T).(arity g c1 t1 a2)) (arity_appl g c1 
138 (lift h d u) a1 (H1 c1 h d H4) (lift h (s (Flat Appl) d) t0) a2 (H3 c1 h (s 
139 (Flat Appl) d) H4)) (lift h d (THead (Flat Appl) u t0)) (lift_head (Flat 
140 Appl) u t0 h d))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a0: 
141 A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1: ((\forall (c1: 
142 C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift 
143 h d u) (asucc g a0)))))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 
144 a0)).(\lambda (H3: ((\forall (c1: C).(\forall (h: nat).(\forall (d: 
145 nat).((drop h d c1 c) \to (arity g c1 (lift h d t0) a0))))))).(\lambda (c1: 
146 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H4: (drop h d c1 
147 c)).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) 
148 t0)) (\lambda (t1: T).(arity g c1 t1 a0)) (arity_cast g c1 (lift h d u) a0 
149 (H1 c1 h d H4) (lift h (s (Flat Cast) d) t0) (H3 c1 h (s (Flat Cast) d) H4)) 
150 (lift h d (THead (Flat Cast) u t0)) (lift_head (Flat Cast) u t0 h 
151 d)))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda 
152 (_: (arity g c t0 a1)).(\lambda (H1: ((\forall (c1: C).(\forall (h: 
153 nat).(\forall (d: nat).((drop h d c1 c) \to (arity g c1 (lift h d t0) 
154 a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c1: 
155 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H3: (drop h d c1 
156 c)).(arity_repl g c1 (lift h d t0) a1 (H1 c1 h d H3) a2 H2)))))))))))) c2 t a 
157 H))))).
158 (* COMMENTS
159 Initial nodes: 2661
160 END *)
161
162 theorem arity_mono:
163  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a1: A).((arity g c 
164 t a1) \to (\forall (a2: A).((arity g c t a2) \to (leq g a1 a2)))))))
165 \def
166  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a1: A).(\lambda (H: 
167 (arity g c t a1)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a: 
168 A).(\forall (a2: A).((arity g c0 t0 a2) \to (leq g a a2)))))) (\lambda (c0: 
169 C).(\lambda (n: nat).(\lambda (a2: A).(\lambda (H0: (arity g c0 (TSort n) 
170 a2)).(leq_sym g a2 (ASort O n) (arity_gen_sort g c0 n a2 H0)))))) (\lambda 
171 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl 
172 i c0 (CHead d (Bind Abbr) u))).(\lambda (a: A).(\lambda (_: (arity g d u 
173 a)).(\lambda (H2: ((\forall (a2: A).((arity g d u a2) \to (leq g a 
174 a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i) a2)).(let H4 
175 \def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T (\lambda (d0: 
176 C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0: 
177 C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda (d0: 
178 C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: 
179 C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2) (\lambda 
180 (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind 
181 Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 
182 a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 
183 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2))) 
184 (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0 
185 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (arity g x0 x1 a2)).(let H8 \def 
186 (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead 
187 x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind 
188 Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C 
189 return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) 
190 \Rightarrow c1])) (CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1) 
191 (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in 
192 ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: 
193 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead 
194 d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) 
195 u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in (\lambda (H11: (eq C d x0)).(let 
196 H12 \def (eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind Abbr) 
197 t0))) H8 u H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity g x0 
198 t0 a2)) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl i c0 
199 (CHead c1 (Bind Abbr) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0 
200 (\lambda (c1: C).(arity g c1 u a2)) H13 d H11) in (H2 a2 H15))))))) H9))))))) 
201 H5)) (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 
202 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 
203 (asucc g a2)))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 
204 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 
205 (asucc g a2)))) (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: 
206 (getl i c0 (CHead x0 (Bind Abst) x1))).(\lambda (_: (arity g x0 x1 (asucc g 
207 a2))).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i 
208 c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i 
209 H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind 
210 Abbr) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with 
211 [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return 
212 (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return 
213 (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | 
214 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind 
215 Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind Abst) 
216 x1) H6)) in (False_ind (leq g a a2) H9))))))) H5)) H4)))))))))))) (\lambda 
217 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl 
218 i c0 (CHead d (Bind Abst) u))).(\lambda (a: A).(\lambda (_: (arity g d u 
219 (asucc g a))).(\lambda (H2: ((\forall (a2: A).((arity g d u a2) \to (leq g 
220 (asucc g a) a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i) 
221 a2)).(let H4 \def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T 
222 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) 
223 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda 
224 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda 
225 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2) 
226 (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead 
227 d0 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 
228 a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 
229 (Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2))) 
230 (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0 
231 (CHead x0 (Bind Abbr) x1))).(\lambda (_: (arity g x0 x1 a2)).(let H8 \def 
232 (eq_ind C (CHead d (Bind Abst) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead 
233 x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind 
234 Abbr) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda 
235 (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
236 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
237 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
238 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void 
239 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abbr) 
240 x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abbr) x1) H6)) 
241 in (False_ind (leq g a a2) H9))))))) H5)) (\lambda (H5: (ex2_2 C T (\lambda 
242 (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda 
243 (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2)))))).(ex2_2_ind C T 
244 (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) 
245 (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2)))) (leq g a a2) 
246 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0 (CHead x0 (Bind 
247 Abst) x1))).(\lambda (H7: (arity g x0 x1 (asucc g a2))).(let H8 \def (eq_ind 
248 C (CHead d (Bind Abst) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead x0 (Bind 
249 Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abst) 
250 x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in C return 
251 (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow 
252 c1])) (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead 
253 d (Bind Abst) u) i H0 (CHead x0 (Bind Abst) x1) H6)) in ((let H10 \def 
254 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with 
255 [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind 
256 Abst) u) (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 
257 (CHead x0 (Bind Abst) x1) H6)) in (\lambda (H11: (eq C d x0)).(let H12 \def 
258 (eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind Abst) t0))) H8 u 
259 H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity g x0 t0 (asucc g 
260 a2))) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl i c0 
261 (CHead c1 (Bind Abst) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0 
262 (\lambda (c1: C).(arity g c1 u (asucc g a2))) H13 d H11) in (asucc_inj g a a2 
263 (H2 (asucc g a2) H15)))))))) H9))))))) H5)) H4)))))))))))) (\lambda (b: 
264 B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c0: C).(\lambda (u: 
265 T).(\lambda (a2: A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall 
266 (a3: A).((arity g c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda 
267 (a3: A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t0 a3)).(\lambda (H4: 
268 ((\forall (a4: A).((arity g (CHead c0 (Bind b) u) t0 a4) \to (leq g a3 
269 a4))))).(\lambda (a0: A).(\lambda (H5: (arity g c0 (THead (Bind b) u t0) 
270 a0)).(let H6 \def (arity_gen_bind b H0 g c0 u t0 a0 H5) in (ex2_ind A 
271 (\lambda (a4: A).(arity g c0 u a4)) (\lambda (_: A).(arity g (CHead c0 (Bind 
272 b) u) t0 a0)) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g c0 u 
273 x)).(\lambda (H8: (arity g (CHead c0 (Bind b) u) t0 a0)).(H4 a0 H8)))) 
274 H6))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2: A).(\lambda 
275 (_: (arity g c0 u (asucc g a2))).(\lambda (H1: ((\forall (a3: A).((arity g c0 
276 u a3) \to (leq g (asucc g a2) a3))))).(\lambda (t0: T).(\lambda (a3: 
277 A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t0 a3)).(\lambda (H3: 
278 ((\forall (a4: A).((arity g (CHead c0 (Bind Abst) u) t0 a4) \to (leq g a3 
279 a4))))).(\lambda (a0: A).(\lambda (H4: (arity g c0 (THead (Bind Abst) u t0) 
280 a0)).(let H5 \def (arity_gen_abst g c0 u t0 a0 H4) in (ex3_2_ind A A (\lambda 
281 (a4: A).(\lambda (a5: A).(eq A a0 (AHead a4 a5)))) (\lambda (a4: A).(\lambda 
282 (_: A).(arity g c0 u (asucc g a4)))) (\lambda (_: A).(\lambda (a5: A).(arity 
283 g (CHead c0 (Bind Abst) u) t0 a5))) (leq g (AHead a2 a3) a0) (\lambda (x0: 
284 A).(\lambda (x1: A).(\lambda (H6: (eq A a0 (AHead x0 x1))).(\lambda (H7: 
285 (arity g c0 u (asucc g x0))).(\lambda (H8: (arity g (CHead c0 (Bind Abst) u) 
286 t0 x1)).(eq_ind_r A (AHead x0 x1) (\lambda (a: A).(leq g (AHead a2 a3) a)) 
287 (leq_head g a2 x0 (asucc_inj g a2 x0 (H1 (asucc g x0) H7)) a3 x1 (H3 x1 H8)) 
288 a0 H6)))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2: 
289 A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall (a3: A).((arity g 
290 c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda (a3: A).(\lambda (_: 
291 (arity g c0 t0 (AHead a2 a3))).(\lambda (H3: ((\forall (a4: A).((arity g c0 
292 t0 a4) \to (leq g (AHead a2 a3) a4))))).(\lambda (a0: A).(\lambda (H4: (arity 
293 g c0 (THead (Flat Appl) u t0) a0)).(let H5 \def (arity_gen_appl g c0 u t0 a0 
294 H4) in (ex2_ind A (\lambda (a4: A).(arity g c0 u a4)) (\lambda (a4: A).(arity 
295 g c0 t0 (AHead a4 a0))) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g 
296 c0 u x)).(\lambda (H7: (arity g c0 t0 (AHead x a0))).(ahead_inj_snd g a2 a3 x 
297 a0 (H3 (AHead x a0) H7))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u: 
298 T).(\lambda (a: A).(\lambda (_: (arity g c0 u (asucc g a))).(\lambda (_: 
299 ((\forall (a2: A).((arity g c0 u a2) \to (leq g (asucc g a) a2))))).(\lambda 
300 (t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2: 
301 A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4: 
302 (arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u 
303 t0 a2 H4) in (land_ind (arity g c0 u (asucc g a2)) (arity g c0 t0 a2) (leq g 
304 a a2) (\lambda (_: (arity g c0 u (asucc g a2))).(\lambda (H7: (arity g c0 t0 
305 a2)).(H3 a2 H7))) H5)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda 
306 (a2: A).(\lambda (_: (arity g c0 t0 a2)).(\lambda (H1: ((\forall (a3: 
307 A).((arity g c0 t0 a3) \to (leq g a2 a3))))).(\lambda (a3: A).(\lambda (H2: 
308 (leq g a2 a3)).(\lambda (a0: A).(\lambda (H3: (arity g c0 t0 a0)).(leq_trans 
309 g a3 a2 (leq_sym g a2 a3 H2) a0 (H1 a0 H3))))))))))) c t a1 H))))).
310 (* COMMENTS
311 Initial nodes: 2947
312 END *)
313
314 theorem arity_repellent:
315  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (t: T).(\forall (a1: 
316 A).((arity g (CHead c (Bind Abst) w) t a1) \to (\forall (a2: A).((arity g c 
317 (THead (Bind Abst) w t) a2) \to ((leq g a1 a2) \to (\forall (P: 
318 Prop).P)))))))))
319 \def
320  \lambda (g: G).(\lambda (c: C).(\lambda (w: T).(\lambda (t: T).(\lambda (a1: 
321 A).(\lambda (H: (arity g (CHead c (Bind Abst) w) t a1)).(\lambda (a2: 
322 A).(\lambda (H0: (arity g c (THead (Bind Abst) w t) a2)).(\lambda (H1: (leq g 
323 a1 a2)).(\lambda (P: Prop).(let H_y \def (arity_repl g (CHead c (Bind Abst) 
324 w) t a1 H a2 H1) in (let H2 \def (arity_gen_abst g c w t a2 H0) in (ex3_2_ind 
325 A A (\lambda (a3: A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: 
326 A).(\lambda (_: A).(arity g c w (asucc g a3)))) (\lambda (_: A).(\lambda (a4: 
327 A).(arity g (CHead c (Bind Abst) w) t a4))) P (\lambda (x0: A).(\lambda (x1: 
328 A).(\lambda (H3: (eq A a2 (AHead x0 x1))).(\lambda (_: (arity g c w (asucc g 
329 x0))).(\lambda (H5: (arity g (CHead c (Bind Abst) w) t x1)).(let H6 \def 
330 (eq_ind A a2 (\lambda (a: A).(arity g (CHead c (Bind Abst) w) t a)) H_y 
331 (AHead x0 x1) H3) in (leq_ahead_false_2 g x1 x0 (arity_mono g (CHead c (Bind 
332 Abst) w) t (AHead x0 x1) H6 x1 H5) P))))))) H2)))))))))))).
333 (* COMMENTS
334 Initial nodes: 283
335 END *)
336
337 theorem arity_appls_cast:
338  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (vs: 
339 TList).(\forall (a: A).((arity g c (THeads (Flat Appl) vs u) (asucc g a)) \to 
340 ((arity g c (THeads (Flat Appl) vs t) a) \to (arity g c (THeads (Flat Appl) 
341 vs (THead (Flat Cast) u t)) a))))))))
342 \def
343  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (vs: 
344 TList).(TList_ind (\lambda (t0: TList).(\forall (a: A).((arity g c (THeads 
345 (Flat Appl) t0 u) (asucc g a)) \to ((arity g c (THeads (Flat Appl) t0 t) a) 
346 \to (arity g c (THeads (Flat Appl) t0 (THead (Flat Cast) u t)) a))))) 
347 (\lambda (a: A).(\lambda (H: (arity g c u (asucc g a))).(\lambda (H0: (arity 
348 g c t a)).(arity_cast g c u a H t H0)))) (\lambda (t0: T).(\lambda (t1: 
349 TList).(\lambda (H: ((\forall (a: A).((arity g c (THeads (Flat Appl) t1 u) 
350 (asucc g a)) \to ((arity g c (THeads (Flat Appl) t1 t) a) \to (arity g c 
351 (THeads (Flat Appl) t1 (THead (Flat Cast) u t)) a)))))).(\lambda (a: 
352 A).(\lambda (H0: (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 u)) 
353 (asucc g a))).(\lambda (H1: (arity g c (THead (Flat Appl) t0 (THeads (Flat 
354 Appl) t1 t)) a)).(let H2 \def (arity_gen_appl g c t0 (THeads (Flat Appl) t1 
355 t) a H1) in (ex2_ind A (\lambda (a1: A).(arity g c t0 a1)) (\lambda (a1: 
356 A).(arity g c (THeads (Flat Appl) t1 t) (AHead a1 a))) (arity g c (THead 
357 (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Flat Cast) u t))) a) (\lambda 
358 (x: A).(\lambda (H3: (arity g c t0 x)).(\lambda (H4: (arity g c (THeads (Flat 
359 Appl) t1 t) (AHead x a))).(let H5 \def (arity_gen_appl g c t0 (THeads (Flat 
360 Appl) t1 u) (asucc g a) H0) in (ex2_ind A (\lambda (a1: A).(arity g c t0 a1)) 
361 (\lambda (a1: A).(arity g c (THeads (Flat Appl) t1 u) (AHead a1 (asucc g 
362 a)))) (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Flat 
363 Cast) u t))) a) (\lambda (x0: A).(\lambda (H6: (arity g c t0 x0)).(\lambda 
364 (H7: (arity g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g 
365 a)))).(arity_appl g c t0 x H3 (THeads (Flat Appl) t1 (THead (Flat Cast) u t)) 
366 a (H (AHead x a) (arity_repl g c (THeads (Flat Appl) t1 u) (AHead x (asucc g 
367 a)) (arity_repl g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g a)) H7 
368 (AHead x (asucc g a)) (leq_head g x0 x (arity_mono g c t0 x0 H6 x H3) (asucc 
369 g a) (asucc g a) (leq_refl g (asucc g a)))) (asucc g (AHead x a)) (leq_refl g 
370 (asucc g (AHead x a)))) H4))))) H5))))) H2)))))))) vs))))).
371 (* COMMENTS
372 Initial nodes: 707
373 END *)
374
375 theorem arity_appls_abbr:
376  \forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
377 nat).((getl i c (CHead d (Bind Abbr) v)) \to (\forall (vs: TList).(\forall 
378 (a: A).((arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a) \to (arity g c 
379 (THeads (Flat Appl) vs (TLRef i)) a)))))))))
380 \def
381  \lambda (g: G).(\lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
382 nat).(\lambda (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (vs: 
383 TList).(TList_ind (\lambda (t: TList).(\forall (a: A).((arity g c (THeads 
384 (Flat Appl) t (lift (S i) O v)) a) \to (arity g c (THeads (Flat Appl) t 
385 (TLRef i)) a)))) (\lambda (a: A).(\lambda (H0: (arity g c (lift (S i) O v) 
386 a)).(arity_abbr g c d v i H a (arity_gen_lift g c v a (S i) O H0 d (getl_drop 
387 Abbr c d v i H))))) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0: 
388 ((\forall (a: A).((arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) a) \to 
389 (arity g c (THeads (Flat Appl) t0 (TLRef i)) a))))).(\lambda (a: A).(\lambda 
390 (H1: (arity g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O 
391 v))) a)).(let H2 \def (arity_gen_appl g c t (THeads (Flat Appl) t0 (lift (S 
392 i) O v)) a H1) in (ex2_ind A (\lambda (a1: A).(arity g c t a1)) (\lambda (a1: 
393 A).(arity g c (THeads (Flat Appl) t0 (lift (S i) O v)) (AHead a1 a))) (arity 
394 g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) a) (\lambda (x: 
395 A).(\lambda (H3: (arity g c t x)).(\lambda (H4: (arity g c (THeads (Flat 
396 Appl) t0 (lift (S i) O v)) (AHead x a))).(arity_appl g c t x H3 (THeads (Flat 
397 Appl) t0 (TLRef i)) a (H0 (AHead x a) H4))))) H2))))))) vs))))))).
398 (* COMMENTS
399 Initial nodes: 425
400 END *)
401
402 theorem arity_appls_bind:
403  \forall (g: G).(\forall (b: B).((not (eq B b Abst)) \to (\forall (c: 
404 C).(\forall (v: T).(\forall (a1: A).((arity g c v a1) \to (\forall (t: 
405 T).(\forall (vs: TList).(\forall (a2: A).((arity g (CHead c (Bind b) v) 
406 (THeads (Flat Appl) (lifts (S O) O vs) t) a2) \to (arity g c (THeads (Flat 
407 Appl) vs (THead (Bind b) v t)) a2)))))))))))
408 \def
409  \lambda (g: G).(\lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda 
410 (c: C).(\lambda (v: T).(\lambda (a1: A).(\lambda (H0: (arity g c v 
411 a1)).(\lambda (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: 
412 TList).(\forall (a2: A).((arity g (CHead c (Bind b) v) (THeads (Flat Appl) 
413 (lifts (S O) O t0) t) a2) \to (arity g c (THeads (Flat Appl) t0 (THead (Bind 
414 b) v t)) a2)))) (\lambda (a2: A).(\lambda (H1: (arity g (CHead c (Bind b) v) 
415 t a2)).(arity_bind g b H c v a1 H0 t a2 H1))) (\lambda (t0: T).(\lambda (t1: 
416 TList).(\lambda (H1: ((\forall (a2: A).((arity g (CHead c (Bind b) v) (THeads 
417 (Flat Appl) (lifts (S O) O t1) t) a2) \to (arity g c (THeads (Flat Appl) t1 
418 (THead (Bind b) v t)) a2))))).(\lambda (a2: A).(\lambda (H2: (arity g (CHead 
419 c (Bind b) v) (THead (Flat Appl) (lift (S O) O t0) (THeads (Flat Appl) (lifts 
420 (S O) O t1) t)) a2)).(let H3 \def (arity_gen_appl g (CHead c (Bind b) v) 
421 (lift (S O) O t0) (THeads (Flat Appl) (lifts (S O) O t1) t) a2 H2) in 
422 (ex2_ind A (\lambda (a3: A).(arity g (CHead c (Bind b) v) (lift (S O) O t0) 
423 a3)) (\lambda (a3: A).(arity g (CHead c (Bind b) v) (THeads (Flat Appl) 
424 (lifts (S O) O t1) t) (AHead a3 a2))) (arity g c (THead (Flat Appl) t0 
425 (THeads (Flat Appl) t1 (THead (Bind b) v t))) a2) (\lambda (x: A).(\lambda 
426 (H4: (arity g (CHead c (Bind b) v) (lift (S O) O t0) x)).(\lambda (H5: (arity 
427 g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O t1) t) (AHead x 
428 a2))).(arity_appl g c t0 x (arity_gen_lift g (CHead c (Bind b) v) t0 x (S O) 
429 O H4 c (drop_drop (Bind b) O c c (drop_refl c) v)) (THeads (Flat Appl) t1 
430 (THead (Bind b) v t)) a2 (H1 (AHead x a2) H5))))) H3))))))) vs))))))))).
431 (* COMMENTS
432 Initial nodes: 567
433 END *)
434