+
+theorem arity_mono:
+ \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a1: A).((arity g c
+t a1) \to (\forall (a2: A).((arity g c t a2) \to (leq g a1 a2)))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a1: A).(\lambda (H:
+(arity g c t a1)).(arity_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (a:
+A).(\forall (a2: A).((arity g c0 t0 a2) \to (leq g a a2)))))) (\lambda (c0:
+C).(\lambda (n: nat).(\lambda (a2: A).(\lambda (H0: (arity g c0 (TSort n)
+a2)).(leq_sym g a2 (ASort O n) (arity_gen_sort g c0 n a2 H0)))))) (\lambda
+(c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl
+i c0 (CHead d (Bind Abbr) u))).(\lambda (a: A).(\lambda (_: (arity g d u
+a)).(\lambda (H2: ((\forall (a2: A).((arity g d u a2) \to (leq g a
+a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i) a2)).(let H4
+\def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T (\lambda (d0:
+C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0:
+C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda (d0:
+C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0:
+C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2) (\lambda
+(H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind
+Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
+a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0
+(Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))
+(leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0
+(CHead x0 (Bind Abbr) x1))).(\lambda (H7: (arity g x0 x1 a2)).(let H8 \def
+(eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead
+x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind
+Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind
+Abbr) u) (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i H0
+(CHead x0 (Bind Abbr) x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0]))
+(CHead d (Bind Abbr) u) (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d
+(Bind Abbr) u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in (\lambda (H11: (eq C d
+x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind
+Abbr) t0))) H8 u H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity
+g x0 t0 a2)) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl
+i c0 (CHead c1 (Bind Abbr) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0
+(\lambda (c1: C).(arity g c1 u a2)) H13 d H11) in (H2 a2 H15))))))) H9)))))))
+H5)) (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0
+(CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
+(asucc g a2)))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0
+(CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
+(asucc g a2)))) (leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6:
+(getl i c0 (CHead x0 (Bind Abst) x1))).(\lambda (_: (arity g x0 x1 (asucc g
+a2))).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c1: C).(getl i
+c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u) i
+H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind
+Abbr) u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with
+[Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) |
+(Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abst) x1) (getl_mono c0
+(CHead d (Bind Abbr) u) i H0 (CHead x0 (Bind Abst) x1) H6)) in (False_ind
+(leq g a a2) H9))))))) H5)) H4)))))))))))) (\lambda (c0: C).(\lambda (d:
+C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind
+Abst) u))).(\lambda (a: A).(\lambda (_: (arity g d u (asucc g a))).(\lambda
+(H2: ((\forall (a2: A).((arity g d u a2) \to (leq g (asucc g a)
+a2))))).(\lambda (a2: A).(\lambda (H3: (arity g c0 (TLRef i) a2)).(let H4
+\def (arity_gen_lref g c0 i a2 H3) in (or_ind (ex2_2 C T (\lambda (d0:
+C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (d0:
+C).(\lambda (u0: T).(arity g d0 u0 a2)))) (ex2_2 C T (\lambda (d0:
+C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0:
+C).(\lambda (u0: T).(arity g d0 u0 (asucc g a2))))) (leq g a a2) (\lambda
+(H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0 (Bind
+Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0
+a2))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u0: T).(getl i c0 (CHead d0
+(Bind Abbr) u0)))) (\lambda (d0: C).(\lambda (u0: T).(arity g d0 u0 a2)))
+(leq g a a2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl i c0
+(CHead x0 (Bind Abbr) x1))).(\lambda (_: (arity g x0 x1 a2)).(let H8 \def
+(eq_ind C (CHead d (Bind Abst) u) (\lambda (c1: C).(getl i c0 c1)) H0 (CHead
+x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind
+Abbr) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abst) u) (\lambda
+(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _)
+\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
+\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
+_) \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d
+(Bind Abst) u) i H0 (CHead x0 (Bind Abbr) x1) H6)) in (False_ind (leq g a a2)
+H9))))))) H5)) (\lambda (H5: (ex2_2 C T (\lambda (d0: C).(\lambda (u0:
+T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda (u0:
+T).(arity g d0 u0 (asucc g a2)))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda
+(u0: T).(getl i c0 (CHead d0 (Bind Abst) u0)))) (\lambda (d0: C).(\lambda
+(u0: T).(arity g d0 u0 (asucc g a2)))) (leq g a a2) (\lambda (x0: C).(\lambda
+(x1: T).(\lambda (H6: (getl i c0 (CHead x0 (Bind Abst) x1))).(\lambda (H7:
+(arity g x0 x1 (asucc g a2))).(let H8 \def (eq_ind C (CHead d (Bind Abst) u)
+(\lambda (c1: C).(getl i c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0
+(CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def
+(f_equal C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead
+c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u) (CHead x0 (Bind Abst) x1)
+(getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead x0 (Bind Abst) x1) H6)) in
+((let H10 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind Abst) u)
+(CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u) i H0 (CHead
+x0 (Bind Abst) x1) H6)) in (\lambda (H11: (eq C d x0)).(let H12 \def
+(eq_ind_r T x1 (\lambda (t0: T).(getl i c0 (CHead x0 (Bind Abst) t0))) H8 u
+H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(arity g x0 t0 (asucc g
+a2))) H7 u H10) in (let H14 \def (eq_ind_r C x0 (\lambda (c1: C).(getl i c0
+(CHead c1 (Bind Abst) u))) H12 d H11) in (let H15 \def (eq_ind_r C x0
+(\lambda (c1: C).(arity g c1 u (asucc g a2))) H13 d H11) in (asucc_inj g a a2
+(H2 (asucc g a2) H15)))))))) H9))))))) H5)) H4)))))))))))) (\lambda (b:
+B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c0: C).(\lambda (u:
+T).(\lambda (a2: A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall
+(a3: A).((arity g c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda
+(a3: A).(\lambda (_: (arity g (CHead c0 (Bind b) u) t0 a3)).(\lambda (H4:
+((\forall (a4: A).((arity g (CHead c0 (Bind b) u) t0 a4) \to (leq g a3
+a4))))).(\lambda (a0: A).(\lambda (H5: (arity g c0 (THead (Bind b) u t0)
+a0)).(let H6 \def (arity_gen_bind b H0 g c0 u t0 a0 H5) in (ex2_ind A
+(\lambda (a4: A).(arity g c0 u a4)) (\lambda (_: A).(arity g (CHead c0 (Bind
+b) u) t0 a0)) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g c0 u
+x)).(\lambda (H8: (arity g (CHead c0 (Bind b) u) t0 a0)).(H4 a0 H8))))
+H6))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2: A).(\lambda
+(_: (arity g c0 u (asucc g a2))).(\lambda (H1: ((\forall (a3: A).((arity g c0
+u a3) \to (leq g (asucc g a2) a3))))).(\lambda (t0: T).(\lambda (a3:
+A).(\lambda (_: (arity g (CHead c0 (Bind Abst) u) t0 a3)).(\lambda (H3:
+((\forall (a4: A).((arity g (CHead c0 (Bind Abst) u) t0 a4) \to (leq g a3
+a4))))).(\lambda (a0: A).(\lambda (H4: (arity g c0 (THead (Bind Abst) u t0)
+a0)).(let H5 \def (arity_gen_abst g c0 u t0 a0 H4) in (ex3_2_ind A A (\lambda
+(a4: A).(\lambda (a5: A).(eq A a0 (AHead a4 a5)))) (\lambda (a4: A).(\lambda
+(_: A).(arity g c0 u (asucc g a4)))) (\lambda (_: A).(\lambda (a5: A).(arity
+g (CHead c0 (Bind Abst) u) t0 a5))) (leq g (AHead a2 a3) a0) (\lambda (x0:
+A).(\lambda (x1: A).(\lambda (H6: (eq A a0 (AHead x0 x1))).(\lambda (H7:
+(arity g c0 u (asucc g x0))).(\lambda (H8: (arity g (CHead c0 (Bind Abst) u)
+t0 x1)).(eq_ind_r A (AHead x0 x1) (\lambda (a: A).(leq g (AHead a2 a3) a))
+(leq_head g a2 x0 (asucc_inj g a2 x0 (H1 (asucc g x0) H7)) a3 x1 (H3 x1 H8))
+a0 H6)))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a2:
+A).(\lambda (_: (arity g c0 u a2)).(\lambda (_: ((\forall (a3: A).((arity g
+c0 u a3) \to (leq g a2 a3))))).(\lambda (t0: T).(\lambda (a3: A).(\lambda (_:
+(arity g c0 t0 (AHead a2 a3))).(\lambda (H3: ((\forall (a4: A).((arity g c0
+t0 a4) \to (leq g (AHead a2 a3) a4))))).(\lambda (a0: A).(\lambda (H4: (arity
+g c0 (THead (Flat Appl) u t0) a0)).(let H5 \def (arity_gen_appl g c0 u t0 a0
+H4) in (ex2_ind A (\lambda (a4: A).(arity g c0 u a4)) (\lambda (a4: A).(arity
+g c0 t0 (AHead a4 a0))) (leq g a3 a0) (\lambda (x: A).(\lambda (_: (arity g
+c0 u x)).(\lambda (H7: (arity g c0 t0 (AHead x a0))).(ahead_inj_snd g a2 a3 x
+a0 (H3 (AHead x a0) H7))))) H5))))))))))))) (\lambda (c0: C).(\lambda (u:
+T).(\lambda (a: A).(\lambda (_: (arity g c0 u (asucc g a))).(\lambda (_:
+((\forall (a2: A).((arity g c0 u a2) \to (leq g (asucc g a) a2))))).(\lambda
+(t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2:
+A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4:
+(arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u
+t0 a2 H4) in (land_ind (arity g c0 u (asucc g a2)) (arity g c0 t0 a2) (leq g
+a a2) (\lambda (_: (arity g c0 u (asucc g a2))).(\lambda (H7: (arity g c0 t0
+a2)).(H3 a2 H7))) H5)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda
+(a2: A).(\lambda (_: (arity g c0 t0 a2)).(\lambda (H1: ((\forall (a3:
+A).((arity g c0 t0 a3) \to (leq g a2 a3))))).(\lambda (a3: A).(\lambda (H2:
+(leq g a2 a3)).(\lambda (a0: A).(\lambda (H3: (arity g c0 t0 a0)).(leq_trans
+g a3 a2 (leq_sym g a2 a3 H2) a0 (H1 a0 H3))))))))))) c t a1 H))))).