matita/matita/contribs/lambdadelta/basic_1A/arity/pr3.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_1A/csuba/arity.ma".
  18
  19 include "basic_1A/pr3/fwd.ma".
  20
  21 include "basic_1A/pr1/fwd.ma".
  22
  23 include "basic_1A/wcpr0/getl.ma".
  24
  25 include "basic_1A/pr0/props.ma".
  26
  27 include "basic_1A/arity/subst0.ma".
  28
  29 lemma arity_sred_wcpr0_pr0:
  30  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g
  31 c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1
  32 t2) \to (arity g c2 t2 a)))))))))
  33 \def
  34  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (a: A).(\lambda
  35 (H: (arity g c1 t1 a)).(arity_ind g (\lambda (c: C).(\lambda (t: T).(\lambda
  36 (a0: A).(\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to
  37 (arity g c2 t2 a0)))))))) (\lambda (c: C).(\lambda (n: nat).(\lambda (c2:
  38 C).(\lambda (_: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H1: (pr0 (TSort n)
  39 t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(arity g c2 t (ASort O n)))
  40 (arity_sort g c2 n) t2 (pr0_gen_sort t2 n H1)))))))) (\lambda (c: C).(\lambda
  41 (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d
  42 (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity g d u a0)).(\lambda
  43 (H2: ((\forall (c2: C).((wcpr0 d c2) \to (\forall (t2: T).((pr0 u t2) \to
  44 (arity g c2 t2 a0))))))).(\lambda (c2: C).(\lambda (H3: (wcpr0 c
  45 c2)).(\lambda (t2: T).(\lambda (H4: (pr0 (TLRef i) t2)).(eq_ind_r T (TLRef i)
  46 (\lambda (t: T).(arity g c2 t a0)) (ex3_2_ind C T (\lambda (e2: C).(\lambda
  47 (u2: T).(getl i c2 (CHead e2 (Bind Abbr) u2)))) (\lambda (e2: C).(\lambda (_:
  48 T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u u2))) (arity g c2
  49 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (getl i c2
  50 (CHead x0 (Bind Abbr) x1))).(\lambda (H6: (wcpr0 d x0)).(\lambda (H7: (pr0 u
  51 x1)).(arity_abbr g c2 x0 x1 i H5 a0 (H2 x0 H6 x1 H7))))))) (wcpr0_getl c c2
  52 H3 i d u (Bind Abbr) H0)) t2 (pr0_gen_lref t2 i H4)))))))))))))) (\lambda (c:
  53 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c
  54 (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity g d u (asucc g
  55 a0))).(\lambda (H2: ((\forall (c2: C).((wcpr0 d c2) \to (\forall (t2:
  56 T).((pr0 u t2) \to (arity g c2 t2 (asucc g a0)))))))).(\lambda (c2:
  57 C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H4: (pr0 (TLRef i)
  58 t2)).(eq_ind_r T (TLRef i) (\lambda (t: T).(arity g c2 t a0)) (ex3_2_ind C T
  59 (\lambda (e2: C).(\lambda (u2: T).(getl i c2 (CHead e2 (Bind Abst) u2))))
  60 (\lambda (e2: C).(\lambda (_: T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2:
  61 T).(pr0 u u2))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1:
  62 T).(\lambda (H5: (getl i c2 (CHead x0 (Bind Abst) x1))).(\lambda (H6: (wcpr0
  63 d x0)).(\lambda (H7: (pr0 u x1)).(arity_abst g c2 x0 x1 i H5 a0 (H2 x0 H6 x1
  64 H7))))))) (wcpr0_getl c c2 H3 i d u (Bind Abst) H0)) t2 (pr0_gen_lref t2 i
  65 H4)))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda
  66 (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u
  67 a1)).(\lambda (H2: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0
  68 u t2) \to (arity g c2 t2 a1))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda
  69 (H3: (arity g (CHead c (Bind b) u) t a2)).(\lambda (H4: ((\forall (c2:
  70 C).((wcpr0 (CHead c (Bind b) u) c2) \to (\forall (t2: T).((pr0 t t2) \to
  71 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H5: (wcpr0 c
  72 c2)).(\lambda (t2: T).(\lambda (H6: (pr0 (THead (Bind b) u t) t2)).(insert_eq
  73 T (THead (Bind b) u t) (\lambda (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g
  74 c2 t2 a2)) (\lambda (y: T).(\lambda (H7: (pr0 y t2)).(pr0_ind (\lambda (t0:
  75 T).(\lambda (t3: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 t3 a2))))
  76 (\lambda (t0: T).(\lambda (H8: (eq T t0 (THead (Bind b) u t))).(let H9 \def
  77 (f_equal T T (\lambda (e: T).e) t0 (THead (Bind b) u t) H8) in (eq_ind_r T
  78 (THead (Bind b) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_bind g b H0
  79 c2 u a1 (H2 c2 H5 u (pr0_refl u)) t a2 (H4 (CHead c2 (Bind b) u) (wcpr0_comp
  80 c c2 H5 u u (pr0_refl u) (Bind b)) t (pr0_refl t))) t0 H9)))) (\lambda (u1:
  81 T).(\lambda (u2: T).(\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (((eq T u1
  82 (THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda
  83 (t4: T).(\lambda (H10: (pr0 t3 t4)).(\lambda (H11: (((eq T t3 (THead (Bind b)
  84 u t)) \to (arity g c2 t4 a2)))).(\lambda (k: K).(\lambda (H12: (eq T (THead k
  85 u1 t3) (THead (Bind b) u t))).(let H13 \def (f_equal T K (\lambda (e:
  86 T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead
  87 k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Bind b) u t) H12) in ((let
  88 H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u1
  89 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3)
  90 (THead (Bind b) u t) H12) in ((let H15 \def (f_equal T T (\lambda (e:
  91 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 |
  92 (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead (Bind b) u t) H12) in
  93 (\lambda (H16: (eq T u1 u)).(\lambda (H17: (eq K k (Bind b))).(eq_ind_r K
  94 (Bind b) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) a2)) (let H18 \def
  95 (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2
  96 t4 a2))) H11 t H15) in (let H19 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0
  97 t4)) H10 t H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).((eq T t0
  98 (THead (Bind b) u t)) \to (arity g c2 u2 a2))) H9 u H16) in (let H21 \def
  99 (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H16) in (arity_bind g b H0 c2
 100 u2 a1 (H2 c2 H5 u2 H21) t4 a2 (H4 (CHead c2 (Bind b) u2) (wcpr0_comp c c2 H5
 101 u u2 H21 (Bind b)) t4 H19)))))) k H17)))) H14)) H13)))))))))))) (\lambda (u0:
 102 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_:
 103 (((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2 a2)))).(\lambda (t3:
 104 T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead
 105 (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H12: (eq T (THead (Flat
 106 Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Bind b) u t))).(let H13 \def
 107 (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee:
 108 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 109 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat
 110 _) \Rightarrow True])])) I (THead (Bind b) u t) H12) in (False_ind (arity g
 111 c2 (THead (Bind Abbr) v2 t4) a2) H13)))))))))))) (\lambda (b0: B).(\lambda
 112 (_: (not (eq B b0 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
 113 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2
 114 a2)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
 115 (_: (((eq T u1 (THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3:
 116 T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead
 117 (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H15: (eq T (THead (Flat
 118 Appl) v1 (THead (Bind b0) u1 t3)) (THead (Bind b) u t))).(let H16 \def
 119 (eq_ind T (THead (Flat Appl) v1 (THead (Bind b0) u1 t3)) (\lambda (ee:
 120 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 121 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat
 122 _) \Rightarrow True])])) I (THead (Bind b) u t) H15) in (False_ind (arity g
 123 c2 (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2)
 124 H16))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (H8: (pr0 u1
 125 u2)).(\lambda (H9: (((eq T u1 (THead (Bind b) u t)) \to (arity g c2 u2
 126 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H10: (pr0 t3 t4)).(\lambda
 127 (H11: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (w:
 128 T).(\lambda (H12: (subst0 O u2 t4 w)).(\lambda (H13: (eq T (THead (Bind Abbr)
 129 u1 t3) (THead (Bind b) u t))).(let H14 \def (f_equal T B (\lambda (e:
 130 T).(match e with [(TSort _) \Rightarrow Abbr | (TLRef _) \Rightarrow Abbr |
 131 (THead k _ _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _)
 132 \Rightarrow Abbr])])) (THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in
 133 ((let H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
 134 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0]))
 135 (THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in ((let H16 \def
 136 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t3 | (TLRef
 137 _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) u1
 138 t3) (THead (Bind b) u t) H13) in (\lambda (H17: (eq T u1 u)).(\lambda (H18:
 139 (eq B Abbr b)).(let H19 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead
 140 (Bind b) u t)) \to (arity g c2 t4 a2))) H11 t H16) in (let H20 \def (eq_ind T
 141 t3 (\lambda (t0: T).(pr0 t0 t4)) H10 t H16) in (let H21 \def (eq_ind T u1
 142 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 u2 a2))) H9
 143 u H17) in (let H22 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H17)
 144 in (let H23 \def (eq_ind_r B b (\lambda (b0: B).((eq T t (THead (Bind b0) u
 145 t)) \to (arity g c2 t4 a2))) H19 Abbr H18) in (let H24 \def (eq_ind_r B b
 146 (\lambda (b0: B).((eq T u (THead (Bind b0) u t)) \to (arity g c2 u2 a2))) H21
 147 Abbr H18) in (let H25 \def (eq_ind_r B b (\lambda (b0: B).(\forall (c3:
 148 C).((wcpr0 (CHead c (Bind b0) u) c3) \to (\forall (t5: T).((pr0 t t5) \to
 149 (arity g c3 t5 a2)))))) H4 Abbr H18) in (let H26 \def (eq_ind_r B b (\lambda
 150 (b0: B).(arity g (CHead c (Bind b0) u) t a2)) H3 Abbr H18) in (let H27 \def
 151 (eq_ind_r B b (\lambda (b0: B).(not (eq B b0 Abst))) H0 Abbr H18) in
 152 (arity_bind g Abbr H27 c2 u2 a1 (H2 c2 H5 u2 H22) w a2 (arity_subst0 g (CHead
 153 c2 (Bind Abbr) u2) t4 a2 (H25 (CHead c2 (Bind Abbr) u2) (wcpr0_comp c c2 H5 u
 154 u2 H22 (Bind Abbr)) t4 H20) c2 u2 O (getl_refl Abbr c2 u2) w
 155 H12)))))))))))))) H15)) H14))))))))))))) (\lambda (b0: B).(\lambda (H8: (not
 156 (eq B b0 Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: (pr0 t3
 157 t4)).(\lambda (H10: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4
 158 a2)))).(\lambda (u0: T).(\lambda (H11: (eq T (THead (Bind b0) u0 (lift (S O)
 159 O t3)) (THead (Bind b) u t))).(let H12 \def (f_equal T B (\lambda (e:
 160 T).(match e with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 |
 161 (THead k _ _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat _)
 162 \Rightarrow b0])])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u
 163 t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
 164 _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow
 165 t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t) H11) in
 166 ((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
 167 \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _)
 168 \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _
 169 t0) \Rightarrow t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b)
 170 u t) H11) in (\lambda (_: (eq T u0 u)).(\lambda (H16: (eq B b0 b)).(let H17
 171 \def (eq_ind B b0 (\lambda (b1: B).(not (eq B b1 Abst))) H8 b H16) in (let
 172 H18 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Bind b) u t0)) \to
 173 (arity g c2 t4 a2))) H10 (lift (S O) O t3) H14) in (let H19 \def (eq_ind_r T
 174 t (\lambda (t0: T).(\forall (c3: C).((wcpr0 (CHead c (Bind b) u) c3) \to
 175 (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 a2)))))) H4 (lift (S O) O
 176 t3) H14) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).(arity g (CHead c
 177 (Bind b) u) t0 a2)) H3 (lift (S O) O t3) H14) in (arity_gen_lift g (CHead c2
 178 (Bind b) u) t4 a2 (S O) O (H19 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H5 u u
 179 (pr0_refl u) (Bind b)) (lift (S O) O t4) (pr0_lift t3 t4 H9 (S O) O)) c2
 180 (drop_drop (Bind b) O c2 c2 (drop_refl c2) u))))))))) H13)) H12))))))))))
 181 (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_:
 182 (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0:
 183 T).(\lambda (H10: (eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t))).(let
 184 H11 \def (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (ee: T).(match ee with
 185 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
 186 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
 187 True])])) I (THead (Bind b) u t) H10) in (False_ind (arity g c2 t4 a2)
 188 H11)))))))) y t2 H7))) H6)))))))))))))))) (\lambda (c: C).(\lambda (u:
 189 T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda (H1:
 190 ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 u t2) \to (arity g
 191 c2 t2 (asucc g a1)))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (H2:
 192 (arity g (CHead c (Bind Abst) u) t a2)).(\lambda (H3: ((\forall (c2:
 193 C).((wcpr0 (CHead c (Bind Abst) u) c2) \to (\forall (t2: T).((pr0 t t2) \to
 194 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c
 195 c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Bind Abst) u t)
 196 t2)).(insert_eq T (THead (Bind Abst) u t) (\lambda (t0: T).(pr0 t0 t2))
 197 (\lambda (_: T).(arity g c2 t2 (AHead a1 a2))) (\lambda (y: T).(\lambda (H6:
 198 (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Bind
 199 Abst) u t)) \to (arity g c2 t3 (AHead a1 a2))))) (\lambda (t0: T).(\lambda
 200 (H7: (eq T t0 (THead (Bind Abst) u t))).(let H8 \def (f_equal T T (\lambda
 201 (e: T).e) t0 (THead (Bind Abst) u t) H7) in (eq_ind_r T (THead (Bind Abst) u
 202 t) (\lambda (t3: T).(arity g c2 t3 (AHead a1 a2))) (arity_head g c2 u a1 (H1
 203 c2 H4 u (pr0_refl u)) t a2 (H3 (CHead c2 (Bind Abst) u) (wcpr0_comp c c2 H4 u
 204 u (pr0_refl u) (Bind Abst)) t (pr0_refl t))) t0 H8)))) (\lambda (u1:
 205 T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1
 206 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2))))).(\lambda (t3:
 207 T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3
 208 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (k:
 209 K).(\lambda (H11: (eq T (THead k u1 t3) (THead (Bind Abst) u t))).(let H12
 210 \def (f_equal T K (\lambda (e: T).(match e with [(TSort _) \Rightarrow k |
 211 (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3)
 212 (THead (Bind Abst) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e:
 213 T).(match e with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 |
 214 (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) (THead (Bind Abst) u t) H11)
 215 in ((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
 216 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0]))
 217 (THead k u1 t3) (THead (Bind Abst) u t) H11) in (\lambda (H15: (eq T u1
 218 u)).(\lambda (H16: (eq K k (Bind Abst))).(eq_ind_r K (Bind Abst) (\lambda
 219 (k0: K).(arity g c2 (THead k0 u2 t4) (AHead a1 a2))) (let H17 \def (eq_ind T
 220 t3 (\lambda (t0: T).((eq T t0 (THead (Bind Abst) u t)) \to (arity g c2 t4
 221 (AHead a1 a2)))) H10 t H14) in (let H18 \def (eq_ind T t3 (\lambda (t0:
 222 T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind T u1 (\lambda (t0: T).((eq
 223 T t0 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2)))) H8 u H15)
 224 in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H7 u H15) in
 225 (arity_head g c2 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 (CHead c2 (Bind Abst) u2)
 226 (wcpr0_comp c c2 H4 u u2 H20 (Bind Abst)) t4 H18)))))) k H16)))) H13))
 227 H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda
 228 (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) \to (arity
 229 g c2 v2 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0
 230 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4
 231 (AHead a1 a2))))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead (Bind
 232 Abst) u0 t3)) (THead (Bind Abst) u t))).(let H12 \def (eq_ind T (THead (Flat
 233 Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with [(TSort
 234 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
 235 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
 236 True])])) I (THead (Bind Abst) u t) H11) in (False_ind (arity g c2 (THead
 237 (Bind Abbr) v2 t4) (AHead a1 a2)) H12)))))))))))) (\lambda (b: B).(\lambda
 238 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
 239 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) \to (arity g c2 v2
 240 (AHead a1 a2))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
 241 u2)).(\lambda (_: (((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2
 242 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3
 243 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4
 244 (AHead a1 a2))))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b)
 245 u1 t3)) (THead (Bind Abst) u t))).(let H15 \def (eq_ind T (THead (Flat Appl)
 246 v1 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _)
 247 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 248 (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I
 249 (THead (Bind Abst) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2
 250 (THead (Flat Appl) (lift (S O) O v2) t4)) (AHead a1 a2)) H15)))))))))))))))))
 251 (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_:
 252 (((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1
 253 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
 254 (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1
 255 a2))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T
 256 (THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t))).(let H13 \def (eq_ind T
 257 (THead (Bind Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _)
 258 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 259 (match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True |
 260 Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow
 261 False])])) I (THead (Bind Abst) u t) H12) in (False_ind (arity g c2 (THead
 262 (Bind Abbr) u2 w) (AHead a1 a2)) H13))))))))))))) (\lambda (b: B).(\lambda
 263 (H7: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0
 264 t3 t4)).(\lambda (H9: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4
 265 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0
 266 (lift (S O) O t3)) (THead (Bind Abst) u t))).(let H11 \def (f_equal T B
 267 (\lambda (e: T).(match e with [(TSort _) \Rightarrow b | (TLRef _)
 268 \Rightarrow b | (THead k _ _) \Rightarrow (match k with [(Bind b0)
 269 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u0 (lift (S O) O
 270 t3)) (THead (Bind Abst) u t) H10) in ((let H12 \def (f_equal T T (\lambda (e:
 271 T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 |
 272 (THead _ t0 _) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead
 273 (Bind Abst) u t) H10) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e
 274 with [(TSort _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3)
 275 | (TLRef _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) |
 276 (THead _ _ t0) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead
 277 (Bind Abst) u t) H10) in (\lambda (_: (eq T u0 u)).(\lambda (H15: (eq B b
 278 Abst)).(let H16 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H7
 279 Abst H15) in (let H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead
 280 (Bind Abst) u t0)) \to (arity g c2 t4 (AHead a1 a2)))) H9 (lift (S O) O t3)
 281 H13) in (let H18 \def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0
 282 (CHead c (Bind Abst) u) c3) \to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3
 283 t5 a2)))))) H3 (lift (S O) O t3) H13) in (let H19 \def (eq_ind_r T t (\lambda
 284 (t0: T).(arity g (CHead c (Bind Abst) u) t0 a2)) H2 (lift (S O) O t3) H13) in
 285 (let H20 \def (match (H16 (refl_equal B Abst)) in False with []) in
 286 H20)))))))) H12)) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda
 287 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity
 288 g c2 t4 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat
 289 Cast) u0 t3) (THead (Bind Abst) u t))).(let H10 \def (eq_ind T (THead (Flat
 290 Cast) u0 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
 291 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind
 292 _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u
 293 t) H9) in (False_ind (arity g c2 t4 (AHead a1 a2)) H10)))))))) y t2 H6)))
 294 H5)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda
 295 (_: (arity g c u a1)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to
 296 (\forall (t2: T).((pr0 u t2) \to (arity g c2 t2 a1))))))).(\lambda (t:
 297 T).(\lambda (a2: A).(\lambda (H2: (arity g c t (AHead a1 a2))).(\lambda (H3:
 298 ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g
 299 c2 t2 (AHead a1 a2)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c
 300 c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Flat Appl) u t)
 301 t2)).(insert_eq T (THead (Flat Appl) u t) (\lambda (t0: T).(pr0 t0 t2))
 302 (\lambda (_: T).(arity g c2 t2 a2)) (\lambda (y: T).(\lambda (H6: (pr0 y
 303 t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Flat Appl)
 304 u t)) \to (arity g c2 t3 a2)))) (\lambda (t0: T).(\lambda (H7: (eq T t0
 305 (THead (Flat Appl) u t))).(let H8 \def (f_equal T T (\lambda (e: T).e) t0
 306 (THead (Flat Appl) u t) H7) in (eq_ind_r T (THead (Flat Appl) u t) (\lambda
 307 (t3: T).(arity g c2 t3 a2)) (arity_appl g c2 u a1 (H1 c2 H4 u (pr0_refl u)) t
 308 a2 (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: T).(\lambda (u2:
 309 T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 (THead (Flat Appl) u
 310 t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9:
 311 (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g
 312 c2 t4 a2)))).(\lambda (k: K).(\lambda (H11: (eq T (THead k u1 t3) (THead
 313 (Flat Appl) u t))).(let H12 \def (f_equal T K (\lambda (e: T).(match e with
 314 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
 315 \Rightarrow k0])) (THead k u1 t3) (THead (Flat Appl) u t) H11) in ((let H13
 316 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u1 |
 317 (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3)
 318 (THead (Flat Appl) u t) H11) in ((let H14 \def (f_equal T T (\lambda (e:
 319 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 |
 320 (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead (Flat Appl) u t) H11)
 321 in (\lambda (H15: (eq T u1 u)).(\lambda (H16: (eq K k (Flat Appl))).(eq_ind_r
 322 K (Flat Appl) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) a2)) (let H17
 323 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to
 324 (arity g c2 t4 a2))) H10 t H14) in (let H18 \def (eq_ind T t3 (\lambda (t0:
 325 T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind T u1 (\lambda (t0: T).((eq
 326 T t0 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2))) H8 u H15) in (let H20
 327 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H7 u H15) in (arity_appl g c2
 328 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 c2 H4 t4 H18)))))) k H16)))) H13))
 329 H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda
 330 (H7: (pr0 v1 v2)).(\lambda (H8: (((eq T v1 (THead (Flat Appl) u t)) \to
 331 (arity g c2 v2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: (pr0 t3
 332 t4)).(\lambda (H10: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4
 333 a2)))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3))
 334 (THead (Flat Appl) u t))).(let H12 \def (f_equal T T (\lambda (e: T).(match e
 335 with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t0 _)
 336 \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead
 337 (Flat Appl) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e
 338 with [(TSort _) \Rightarrow (THead (Bind Abst) u0 t3) | (TLRef _) \Rightarrow
 339 (THead (Bind Abst) u0 t3) | (THead _ _ t0) \Rightarrow t0])) (THead (Flat
 340 Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) u t) H11) in (\lambda
 341 (H14: (eq T v1 u)).(let H15 \def (eq_ind T v1 (\lambda (t0: T).((eq T t0
 342 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2))) H8 u H14) in (let H16 \def
 343 (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2)) H7 u H14) in (let H17 \def
 344 (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Flat Appl) u t0)) \to (arity
 345 g c2 t4 a2))) H10 (THead (Bind Abst) u0 t3) H13) in (let H18 \def (eq_ind_r T
 346 t (\lambda (t0: T).((eq T u (THead (Flat Appl) u t0)) \to (arity g c2 v2
 347 a2))) H15 (THead (Bind Abst) u0 t3) H13) in (let H19 \def (eq_ind_r T t
 348 (\lambda (t0: T).(\forall (c3: C).((wcpr0 c c3) \to (\forall (t5: T).((pr0 t0
 349 t5) \to (arity g c3 t5 (AHead a1 a2))))))) H3 (THead (Bind Abst) u0 t3) H13)
 350 in (let H20 \def (eq_ind_r T t (\lambda (t0: T).(arity g c t0 (AHead a1 a2)))
 351 H2 (THead (Bind Abst) u0 t3) H13) in (let H21 \def (H1 c2 H4 v2 H16) in (let
 352 H22 \def (H19 c2 H4 (THead (Bind Abst) u0 t4) (pr0_comp u0 u0 (pr0_refl u0)
 353 t3 t4 H9 (Bind Abst))) in (let H23 \def (arity_gen_abst g c2 u0 t4 (AHead a1
 354 a2) H22) in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq A (AHead a1
 355 a2) (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(arity g c2 u0 (asucc g
 356 a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g (CHead c2 (Bind Abst) u0) t4
 357 a4))) (arity g c2 (THead (Bind Abbr) v2 t4) a2) (\lambda (x0: A).(\lambda
 358 (x1: A).(\lambda (H24: (eq A (AHead a1 a2) (AHead x0 x1))).(\lambda (H25:
 359 (arity g c2 u0 (asucc g x0))).(\lambda (H26: (arity g (CHead c2 (Bind Abst)
 360 u0) t4 x1)).(let H27 \def (f_equal A A (\lambda (e: A).(match e with [(ASort
 361 _ _) \Rightarrow a1 | (AHead a0 _) \Rightarrow a0])) (AHead a1 a2) (AHead x0
 362 x1) H24) in ((let H28 \def (f_equal A A (\lambda (e: A).(match e with [(ASort
 363 _ _) \Rightarrow a2 | (AHead _ a0) \Rightarrow a0])) (AHead a1 a2) (AHead x0
 364 x1) H24) in (\lambda (H29: (eq A a1 x0)).(let H30 \def (eq_ind_r A x1
 365 (\lambda (a0: A).(arity g (CHead c2 (Bind Abst) u0) t4 a0)) H26 a2 H28) in
 366 (let H31 \def (eq_ind_r A x0 (\lambda (a0: A).(arity g c2 u0 (asucc g a0)))
 367 H25 a1 H29) in (arity_bind g Abbr not_abbr_abst c2 v2 a1 H21 t4 a2
 368 (csuba_arity g (CHead c2 (Bind Abst) u0) t4 a2 H30 (CHead c2 (Bind Abbr) v2)
 369 (csuba_abst g c2 c2 (csuba_refl g c2) u0 a1 H31 v2 H21))))))) H27)))))))
 370 H23)))))))))))) H12)))))))))))) (\lambda (b: B).(\lambda (H7: (not (eq B b
 371 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H8: (pr0 v1 v2)).(\lambda
 372 (H9: (((eq T v1 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2)))).(\lambda
 373 (u1: T).(\lambda (u2: T).(\lambda (H10: (pr0 u1 u2)).(\lambda (H11: (((eq T
 374 u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3:
 375 T).(\lambda (t4: T).(\lambda (H12: (pr0 t3 t4)).(\lambda (H13: (((eq T t3
 376 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (H14: (eq T
 377 (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t))).(let
 378 H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v1
 379 | (TLRef _) \Rightarrow v1 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat
 380 Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t) H14) in ((let H16
 381 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead
 382 (Bind b) u1 t3) | (TLRef _) \Rightarrow (THead (Bind b) u1 t3) | (THead _ _
 383 t0) \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead
 384 (Flat Appl) u t) H14) in (\lambda (H17: (eq T v1 u)).(let H18 \def (eq_ind T
 385 v1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 v2
 386 a2))) H9 u H17) in (let H19 \def (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2))
 387 H8 u H17) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead
 388 (Flat Appl) u t0)) \to (arity g c2 t4 a2))) H13 (THead (Bind b) u1 t3) H16)
 389 in (let H21 \def (eq_ind_r T t (\lambda (t0: T).((eq T u1 (THead (Flat Appl)
 390 u t0)) \to (arity g c2 u2 a2))) H11 (THead (Bind b) u1 t3) H16) in (let H22
 391 \def (eq_ind_r T t (\lambda (t0: T).((eq T u (THead (Flat Appl) u t0)) \to
 392 (arity g c2 v2 a2))) H18 (THead (Bind b) u1 t3) H16) in (let H23 \def
 393 (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 c c3) \to (\forall
 394 (t5: T).((pr0 t0 t5) \to (arity g c3 t5 (AHead a1 a2))))))) H3 (THead (Bind
 395 b) u1 t3) H16) in (let H24 \def (eq_ind_r T t (\lambda (t0: T).(arity g c t0
 396 (AHead a1 a2))) H2 (THead (Bind b) u1 t3) H16) in (let H25 \def (H1 c2 H4 v2
 397 H19) in (let H26 \def (H23 c2 H4 (THead (Bind b) u2 t4) (pr0_comp u1 u2 H10
 398 t3 t4 H12 (Bind b))) in (let H27 \def (arity_gen_bind b H7 g c2 u2 t4 (AHead
 399 a1 a2) H26) in (ex2_ind A (\lambda (a3: A).(arity g c2 u2 a3)) (\lambda (_:
 400 A).(arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2))) (arity g c2 (THead
 401 (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2) (\lambda (x:
 402 A).(\lambda (H28: (arity g c2 u2 x)).(\lambda (H29: (arity g (CHead c2 (Bind
 403 b) u2) t4 (AHead a1 a2))).(arity_bind g b H7 c2 u2 x H28 (THead (Flat Appl)
 404 (lift (S O) O v2) t4) a2 (arity_appl g (CHead c2 (Bind b) u2) (lift (S O) O
 405 v2) a1 (arity_lift g c2 v2 a1 H25 (CHead c2 (Bind b) u2) (S O) O (drop_drop
 406 (Bind b) O c2 c2 (drop_refl c2) u2)) t4 a2 H29))))) H27)))))))))))))
 407 H15))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
 408 u2)).(\lambda (_: (((eq T u1 (THead (Flat Appl) u t)) \to (arity g c2 u2
 409 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
 410 (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda
 411 (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T (THead (Bind
 412 Abbr) u1 t3) (THead (Flat Appl) u t))).(let H13 \def (eq_ind T (THead (Bind
 413 Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
 414 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind
 415 _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u
 416 t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) u2 w) a2)
 417 H13))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
 418 (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3
 419 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0: T).(\lambda
 420 (H10: (eq T (THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Appl) u
 421 t))).(let H11 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O t3)) (\lambda
 422 (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
 423 False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True |
 424 (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u t) H10) in (False_ind
 425 (arity g c2 t4 a2) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda
 426 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity
 427 g c2 t4 a2)))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat Cast) u0 t3)
 428 (THead (Flat Appl) u t))).(let H10 \def (eq_ind T (THead (Flat Cast) u0 t3)
 429 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
 430 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
 431 \Rightarrow False | (Flat f) \Rightarrow (match f with [Appl \Rightarrow
 432 False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t) H9) in
 433 (False_ind (arity g c2 t4 a2) H10)))))))) y t2 H6))) H5))))))))))))))
 434 (\lambda (c: C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c u
 435 (asucc g a0))).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall
 436 (t2: T).((pr0 u t2) \to (arity g c2 t2 (asucc g a0)))))))).(\lambda (t:
 437 T).(\lambda (_: (arity g c t a0)).(\lambda (H3: ((\forall (c2: C).((wcpr0 c
 438 c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 a0))))))).(\lambda
 439 (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H5: (pr0
 440 (THead (Flat Cast) u t) t2)).(insert_eq T (THead (Flat Cast) u t) (\lambda
 441 (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g c2 t2 a0)) (\lambda (y:
 442 T).(\lambda (H6: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq
 443 T t0 (THead (Flat Cast) u t)) \to (arity g c2 t3 a0)))) (\lambda (t0:
 444 T).(\lambda (H7: (eq T t0 (THead (Flat Cast) u t))).(let H8 \def (f_equal T T
 445 (\lambda (e: T).e) t0 (THead (Flat Cast) u t) H7) in (eq_ind_r T (THead (Flat
 446 Cast) u t) (\lambda (t3: T).(arity g c2 t3 a0)) (arity_cast g c2 u a0 (H1 c2
 447 H4 u (pr0_refl u)) t (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1:
 448 T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1
 449 (THead (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda
 450 (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat
 451 Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (k: K).(\lambda (H11: (eq T
 452 (THead k u1 t3) (THead (Flat Cast) u t))).(let H12 \def (f_equal T K (\lambda
 453 (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k |
 454 (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Flat Cast) u t) H11)
 455 in ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
 456 \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0]))
 457 (THead k u1 t3) (THead (Flat Cast) u t) H11) in ((let H14 \def (f_equal T T
 458 (\lambda (e: T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _)
 459 \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead
 460 (Flat Cast) u t) H11) in (\lambda (H15: (eq T u1 u)).(\lambda (H16: (eq K k
 461 (Flat Cast))).(eq_ind_r K (Flat Cast) (\lambda (k0: K).(arity g c2 (THead k0
 462 u2 t4) a0)) (let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead
 463 (Flat Cast) u t)) \to (arity g c2 t4 a0))) H10 t H14) in (let H18 \def
 464 (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind
 465 T u1 (\lambda (t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 u2
 466 a0))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2))
 467 H7 u H15) in (arity_cast g c2 u2 a0 (H1 c2 H4 u2 H20) t4 (H3 c2 H4 t4
 468 H18)))))) k H16)))) H13)) H12)))))))))))) (\lambda (u0: T).(\lambda (v1:
 469 T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead
 470 (Flat Cast) u t)) \to (arity g c2 v2 a0)))).(\lambda (t3: T).(\lambda (t4:
 471 T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t))
 472 \to (arity g c2 t4 a0)))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead
 473 (Bind Abst) u0 t3)) (THead (Flat Cast) u t))).(let H12 \def (eq_ind T (THead
 474 (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with
 475 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
 476 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow
 477 (match f with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead
 478 (Flat Cast) u t) H11) in (False_ind (arity g c2 (THead (Bind Abbr) v2 t4) a0)
 479 H12)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
 480 (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1
 481 (THead (Flat Cast) u t)) \to (arity g c2 v2 a0)))).(\lambda (u1: T).(\lambda
 482 (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Flat Cast)
 483 u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda
 484 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity
 485 g c2 t4 a0)))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1
 486 t3)) (THead (Flat Cast) u t))).(let H15 \def (eq_ind T (THead (Flat Appl) v1
 487 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _)
 488 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 489 (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
 490 with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat
 491 Cast) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 (THead (Flat
 492 Appl) (lift (S O) O v2) t4)) a0) H15))))))))))))))))) (\lambda (u1:
 493 T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead
 494 (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4:
 495 T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t))
 496 \to (arity g c2 t4 a0)))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4
 497 w)).(\lambda (H12: (eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u
 498 t))).(let H13 \def (eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (ee:
 499 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 500 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat
 501 _) \Rightarrow False])])) I (THead (Flat Cast) u t) H12) in (False_ind (arity
 502 g c2 (THead (Bind Abbr) u2 w) a0) H13))))))))))))) (\lambda (b: B).(\lambda
 503 (_: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0
 504 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity g c2 t4
 505 a0)))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0 (lift (S O) O
 506 t3)) (THead (Flat Cast) u t))).(let H11 \def (eq_ind T (THead (Bind b) u0
 507 (lift (S O) O t3)) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
 508 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with
 509 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat
 510 Cast) u t) H10) in (False_ind (arity g c2 t4 a0) H11)))))))))) (\lambda (t3:
 511 T).(\lambda (t4: T).(\lambda (H7: (pr0 t3 t4)).(\lambda (H8: (((eq T t3
 512 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (u0: T).(\lambda
 513 (H9: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t))).(let H10 \def
 514 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef
 515 _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Cast) u0
 516 t3) (THead (Flat Cast) u t) H9) in ((let H11 \def (f_equal T T (\lambda (e:
 517 T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 |
 518 (THead _ _ t0) \Rightarrow t0])) (THead (Flat Cast) u0 t3) (THead (Flat Cast)
 519 u t) H9) in (\lambda (_: (eq T u0 u)).(let H13 \def (eq_ind T t3 (\lambda
 520 (t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0))) H8 t H11)
 521 in (let H14 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H7 t H11) in (H3
 522 c2 H4 t4 H14))))) H10)))))))) y t2 H6))) H5))))))))))))) (\lambda (c:
 523 C).(\lambda (t: T).(\lambda (a1: A).(\lambda (_: (arity g c t a1)).(\lambda
 524 (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to
 525 (arity g c2 t2 a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1
 526 a2)).(\lambda (c2: C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda
 527 (H4: (pr0 t t2)).(arity_repl g c2 t2 a1 (H1 c2 H3 t2 H4) a2 H2)))))))))))) c1
 528 t1 a H))))).
 529
 530 lemma arity_sred_wcpr0_pr1:
 531  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall
 532 (c1: C).(\forall (a: A).((arity g c1 t1 a) \to (\forall (c2: C).((wcpr0 c1
 533 c2) \to (arity g c2 t2 a)))))))))
 534 \def
 535  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1 t2)).(pr1_ind (\lambda
 536 (t: T).(\lambda (t0: T).(\forall (g: G).(\forall (c1: C).(\forall (a:
 537 A).((arity g c1 t a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (arity g c2 t0
 538 a))))))))) (\lambda (t: T).(\lambda (g: G).(\lambda (c1: C).(\lambda (a:
 539 A).(\lambda (H0: (arity g c1 t a)).(\lambda (c2: C).(\lambda (H1: (wcpr0 c1
 540 c2)).(arity_sred_wcpr0_pr0 g c1 t a H0 c2 H1 t (pr0_refl t))))))))) (\lambda
 541 (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t4 t3)).(\lambda (t5: T).(\lambda
 542 (_: (pr1 t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (c1: C).(\forall (a:
 543 A).((arity g c1 t3 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (arity g c2 t5
 544 a))))))))).(\lambda (g: G).(\lambda (c1: C).(\lambda (a: A).(\lambda (H3:
 545 (arity g c1 t4 a)).(\lambda (c2: C).(\lambda (H4: (wcpr0 c1 c2)).(H2 g c2 a
 546 (arity_sred_wcpr0_pr0 g c1 t4 a H3 c2 H4 t3 H0) c2 (wcpr0_refl
 547 c2)))))))))))))) t1 t2 H))).
 548
 549 lemma arity_sred_pr2:
 550  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
 551 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
 552 \def
 553  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
 554 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (g:
 555 G).(\forall (a: A).((arity g c0 t a) \to (arity g c0 t0 a))))))) (\lambda
 556 (c0: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda
 557 (g: G).(\lambda (a: A).(\lambda (H1: (arity g c0 t3 a)).(arity_sred_wcpr0_pr0
 558 g c0 t3 a H1 c0 (wcpr0_refl c0) t4 H0)))))))) (\lambda (c0: C).(\lambda (d:
 559 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind
 560 Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3
 561 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g:
 562 G).(\lambda (a: A).(\lambda (H3: (arity g c0 t3 a)).(arity_subst0 g c0 t4 a
 563 (arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t
 564 H2)))))))))))))) c t1 t2 H)))).
 565
 566 lemma arity_sred_pr3:
 567  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall
 568 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
 569 \def
 570  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1
 571 t2)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (g: G).(\forall (a:
 572 A).((arity g c t a) \to (arity g c t0 a)))))) (\lambda (t: T).(\lambda (g:
 573 G).(\lambda (a: A).(\lambda (H0: (arity g c t a)).H0)))) (\lambda (t3:
 574 T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
 575 (_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (a: A).((arity g c
 576 t3 a) \to (arity g c t5 a)))))).(\lambda (g: G).(\lambda (a: A).(\lambda (H3:
 577 (arity g c t4 a)).(H2 g a (arity_sred_pr2 c t4 t3 H0 g a H3))))))))))) t1 t2
 578 H)))).
 579