matita/matita/contribs/lambdadelta/basic_1/csuba/arity.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/csuba/getl.ma".
  18
  19 include "basic_1/csuba/props.ma".
  20
  21 include "basic_1/arity/fwd.ma".
  22
  23 include "basic_1/csubv/getl.ma".
  24
  25 theorem csuba_arity:
  26  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1
  27 t a) \to (\forall (c2: C).((csuba g c1 c2) \to (arity g c2 t a)))))))
  28 \def
  29  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
  30 (arity g c1 t a)).(let TMP_1 \def (\lambda (c: C).(\lambda (t0: T).(\lambda
  31 (a0: A).(\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 a0)))))) in (let
  32 TMP_2 \def (\lambda (c: C).(\lambda (n: nat).(\lambda (c2: C).(\lambda (_:
  33 (csuba g c c2)).(arity_sort g c2 n))))) in (let TMP_11 \def (\lambda (c:
  34 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c
  35 (CHead d (Bind Abbr) u))).(\lambda (a0: A).(\lambda (_: (arity g d u
  36 a0)).(\lambda (H2: ((\forall (c2: C).((csuba g d c2) \to (arity g c2 u
  37 a0))))).(\lambda (c2: C).(\lambda (H3: (csuba g c c2)).(let H4 \def
  38 (csuba_getl_abbr g c d u i H0 c2 H3) in (let TMP_5 \def (\lambda (d2: C).(let
  39 TMP_3 \def (Bind Abbr) in (let TMP_4 \def (CHead d2 TMP_3 u) in (getl i c2
  40 TMP_4)))) in (let TMP_6 \def (\lambda (d2: C).(csuba g d d2)) in (let TMP_7
  41 \def (TLRef i) in (let TMP_8 \def (arity g c2 TMP_7 a0) in (let TMP_10 \def
  42 (\lambda (x: C).(\lambda (H5: (getl i c2 (CHead x (Bind Abbr) u))).(\lambda
  43 (H6: (csuba g d x)).(let TMP_9 \def (H2 x H6) in (arity_abbr g c2 x u i H5 a0
  44 TMP_9))))) in (ex2_ind C TMP_5 TMP_6 TMP_8 TMP_10 H4))))))))))))))))) in (let
  45 TMP_53 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i:
  46 nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0:
  47 A).(\lambda (H1: (arity g d u (asucc g a0))).(\lambda (H2: ((\forall (c2:
  48 C).((csuba g d c2) \to (arity g c2 u (asucc g a0)))))).(\lambda (c2:
  49 C).(\lambda (H3: (csuba g c c2)).(let H4 \def (csuba_getl_abst g c d u i H0
  50 c2 H3) in (let TMP_14 \def (\lambda (d2: C).(let TMP_12 \def (Bind Abst) in
  51 (let TMP_13 \def (CHead d2 TMP_12 u) in (getl i c2 TMP_13)))) in (let TMP_15
  52 \def (\lambda (d2: C).(csuba g d d2)) in (let TMP_16 \def (ex2 C TMP_14
  53 TMP_15) in (let TMP_19 \def (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
  54 A).(let TMP_17 \def (Bind Abbr) in (let TMP_18 \def (CHead d2 TMP_17 u2) in
  55 (getl i c2 TMP_18)))))) in (let TMP_20 \def (\lambda (d2: C).(\lambda (_:
  56 T).(\lambda (_: A).(csuba g d d2)))) in (let TMP_22 \def (\lambda (_:
  57 C).(\lambda (_: T).(\lambda (a1: A).(let TMP_21 \def (asucc g a1) in (arity g
  58 d u TMP_21))))) in (let TMP_23 \def (\lambda (d2: C).(\lambda (u2:
  59 T).(\lambda (a1: A).(arity g d2 u2 a1)))) in (let TMP_24 \def (ex4_3 C T A
  60 TMP_19 TMP_20 TMP_22 TMP_23) in (let TMP_25 \def (TLRef i) in (let TMP_26
  61 \def (arity g c2 TMP_25 a0) in (let TMP_35 \def (\lambda (H5: (ex2 C (\lambda
  62 (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d
  63 d2)))).(let TMP_29 \def (\lambda (d2: C).(let TMP_27 \def (Bind Abst) in (let
  64 TMP_28 \def (CHead d2 TMP_27 u) in (getl i c2 TMP_28)))) in (let TMP_30 \def
  65 (\lambda (d2: C).(csuba g d d2)) in (let TMP_31 \def (TLRef i) in (let TMP_32
  66 \def (arity g c2 TMP_31 a0) in (let TMP_34 \def (\lambda (x: C).(\lambda (H6:
  67 (getl i c2 (CHead x (Bind Abst) u))).(\lambda (H7: (csuba g d x)).(let TMP_33
  68 \def (H2 x H7) in (arity_abst g c2 x u i H6 a0 TMP_33))))) in (ex2_ind C
  69 TMP_29 TMP_30 TMP_32 TMP_34 H5))))))) in (let TMP_52 \def (\lambda (H5:
  70 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
  71 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
  72 A).(csuba g d d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity
  73 g d u (asucc g a1))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1:
  74 A).(arity g d2 u2 a1)))))).(let TMP_38 \def (\lambda (d2: C).(\lambda (u2:
  75 T).(\lambda (_: A).(let TMP_36 \def (Bind Abbr) in (let TMP_37 \def (CHead d2
  76 TMP_36 u2) in (getl i c2 TMP_37)))))) in (let TMP_39 \def (\lambda (d2:
  77 C).(\lambda (_: T).(\lambda (_: A).(csuba g d d2)))) in (let TMP_41 \def
  78 (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(let TMP_40 \def (asucc g
  79 a1) in (arity g d u TMP_40))))) in (let TMP_42 \def (\lambda (d2: C).(\lambda
  80 (u2: T).(\lambda (a1: A).(arity g d2 u2 a1)))) in (let TMP_43 \def (TLRef i)
  81 in (let TMP_44 \def (arity g c2 TMP_43 a0) in (let TMP_51 \def (\lambda (x0:
  82 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H6: (getl i c2 (CHead x0 (Bind
  83 Abbr) x1))).(\lambda (_: (csuba g d x0)).(\lambda (H8: (arity g d u (asucc g
  84 x2))).(\lambda (H9: (arity g x0 x1 x2)).(let TMP_45 \def (TLRef i) in (let
  85 TMP_46 \def (arity_abbr g c2 x0 x1 i H6 x2 H9) in (let TMP_47 \def (asucc g
  86 x2) in (let TMP_48 \def (asucc g a0) in (let TMP_49 \def (arity_mono g d u
  87 TMP_47 H8 TMP_48 H1) in (let TMP_50 \def (asucc_inj g x2 a0 TMP_49) in
  88 (arity_repl g c2 TMP_45 x2 TMP_46 a0 TMP_50)))))))))))))) in (ex4_3_ind C T A
  89 TMP_38 TMP_39 TMP_41 TMP_42 TMP_44 TMP_51 H5))))))))) in (or_ind TMP_16
  90 TMP_24 TMP_26 TMP_35 TMP_52 H4)))))))))))))))))))))))) in (let TMP_60 \def
  91 (\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda
  92 (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2:
  93 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u a1))))).(\lambda (t0:
  94 T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0
  95 a2)).(\lambda (H4: ((\forall (c2: C).((csuba g (CHead c (Bind b) u) c2) \to
  96 (arity g c2 t0 a2))))).(\lambda (c2: C).(\lambda (H5: (csuba g c c2)).(let
  97 TMP_54 \def (H2 c2 H5) in (let TMP_55 \def (Bind b) in (let TMP_56 \def
  98 (CHead c2 TMP_55 u) in (let TMP_57 \def (Bind b) in (let TMP_58 \def
  99 (csuba_head g c c2 H5 TMP_57 u) in (let TMP_59 \def (H4 TMP_56 TMP_58) in
 100 (arity_bind g b H0 c2 u a1 TMP_54 t0 a2 TMP_59)))))))))))))))))))) in (let
 101 TMP_67 \def (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_:
 102 (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c2: C).((csuba g c c2)
 103 \to (arity g c2 u (asucc g a1)))))).(\lambda (t0: T).(\lambda (a2:
 104 A).(\lambda (_: (arity g (CHead c (Bind Abst) u) t0 a2)).(\lambda (H3:
 105 ((\forall (c2: C).((csuba g (CHead c (Bind Abst) u) c2) \to (arity g c2 t0
 106 a2))))).(\lambda (c2: C).(\lambda (H4: (csuba g c c2)).(let TMP_61 \def (H1
 107 c2 H4) in (let TMP_62 \def (Bind Abst) in (let TMP_63 \def (CHead c2 TMP_62
 108 u) in (let TMP_64 \def (Bind Abst) in (let TMP_65 \def (csuba_head g c c2 H4
 109 TMP_64 u) in (let TMP_66 \def (H3 TMP_63 TMP_65) in (arity_head g c2 u a1
 110 TMP_61 t0 a2 TMP_66)))))))))))))))))) in (let TMP_70 \def (\lambda (c:
 111 C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda
 112 (H1: ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u a1))))).(\lambda
 113 (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda
 114 (H3: ((\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 (AHead a1
 115 a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c c2)).(let TMP_68 \def (H1
 116 c2 H4) in (let TMP_69 \def (H3 c2 H4) in (arity_appl g c2 u a1 TMP_68 t0 a2
 117 TMP_69)))))))))))))) in (let TMP_73 \def (\lambda (c: C).(\lambda (u:
 118 T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1:
 119 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 u (asucc g
 120 a0)))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3:
 121 ((\forall (c2: C).((csuba g c c2) \to (arity g c2 t0 a0))))).(\lambda (c2:
 122 C).(\lambda (H4: (csuba g c c2)).(let TMP_71 \def (H1 c2 H4) in (let TMP_72
 123 \def (H3 c2 H4) in (arity_cast g c2 u a0 TMP_71 t0 TMP_72))))))))))))) in
 124 (let TMP_75 \def (\lambda (c: C).(\lambda (t0: T).(\lambda (a1: A).(\lambda
 125 (_: (arity g c t0 a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c c2) \to
 126 (arity g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda
 127 (c2: C).(\lambda (H3: (csuba g c c2)).(let TMP_74 \def (H1 c2 H3) in
 128 (arity_repl g c2 t0 a1 TMP_74 a2 H2))))))))))) in (arity_ind g TMP_1 TMP_2
 129 TMP_11 TMP_53 TMP_60 TMP_67 TMP_70 TMP_73 TMP_75 c1 t a H)))))))))))))).
 130
 131 theorem csuba_arity_rev:
 132  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1
 133 t a) \to (\forall (c2: C).((csuba g c2 c1) \to ((csubv c2 c1) \to (arity g c2
 134 t a))))))))
 135 \def
 136  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
 137 (arity g c1 t a)).(let TMP_1 \def (\lambda (c: C).(\lambda (t0: T).(\lambda
 138 (a0: A).(\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0
 139 a0))))))) in (let TMP_2 \def (\lambda (c: C).(\lambda (n: nat).(\lambda (c2:
 140 C).(\lambda (_: (csuba g c2 c)).(\lambda (_: (csubv c2 c)).(arity_sort g c2
 141 n)))))) in (let TMP_142 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u:
 142 T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr)
 143 u))).(\lambda (a0: A).(\lambda (H1: (arity g d u a0)).(\lambda (H2: ((\forall
 144 (c2: C).((csuba g c2 d) \to ((csubv c2 d) \to (arity g c2 u a0)))))).(\lambda
 145 (c2: C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let H_x
 146 \def (csuba_getl_abbr_rev g c d u i H0 c2 H3) in (let H5 \def H_x in (let
 147 TMP_5 \def (\lambda (d2: C).(let TMP_3 \def (Bind Abbr) in (let TMP_4 \def
 148 (CHead d2 TMP_3 u) in (getl i c2 TMP_4)))) in (let TMP_6 \def (\lambda (d2:
 149 C).(csuba g d2 d)) in (let TMP_7 \def (ex2 C TMP_5 TMP_6) in (let TMP_10 \def
 150 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(let TMP_8 \def (Bind Abst)
 151 in (let TMP_9 \def (CHead d2 TMP_8 u2) in (getl i c2 TMP_9)))))) in (let
 152 TMP_11 \def (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
 153 d)))) in (let TMP_13 \def (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1:
 154 A).(let TMP_12 \def (asucc g a1) in (arity g d2 u2 TMP_12))))) in (let TMP_14
 155 \def (\lambda (_: C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1)))) in
 156 (let TMP_15 \def (ex4_3 C T A TMP_10 TMP_11 TMP_13 TMP_14) in (let TMP_18
 157 \def (\lambda (d2: C).(\lambda (u2: T).(let TMP_16 \def (Bind Void) in (let
 158 TMP_17 \def (CHead d2 TMP_16 u2) in (getl i c2 TMP_17))))) in (let TMP_19
 159 \def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_20 \def
 160 (ex2_2 C T TMP_18 TMP_19) in (let TMP_21 \def (TLRef i) in (let TMP_22 \def
 161 (arity g c2 TMP_21 a0) in (let TMP_90 \def (\lambda (H6: (ex2 C (\lambda (d2:
 162 C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d2
 163 d)))).(let TMP_25 \def (\lambda (d2: C).(let TMP_23 \def (Bind Abbr) in (let
 164 TMP_24 \def (CHead d2 TMP_23 u) in (getl i c2 TMP_24)))) in (let TMP_26 \def
 165 (\lambda (d2: C).(csuba g d2 d)) in (let TMP_27 \def (TLRef i) in (let TMP_28
 166 \def (arity g c2 TMP_27 a0) in (let TMP_89 \def (\lambda (x: C).(\lambda (H7:
 167 (getl i c2 (CHead x (Bind Abbr) u))).(\lambda (H8: (csuba g x d)).(let H_x0
 168 \def (csubv_getl_conf c2 c H4 Abbr x u i H7) in (let H9 \def H_x0 in (let
 169 TMP_29 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2))))
 170 in (let TMP_32 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let
 171 TMP_30 \def (Bind b2) in (let TMP_31 \def (CHead d2 TMP_30 v2) in (getl i c
 172 TMP_31)))))) in (let TMP_33 \def (TLRef i) in (let TMP_34 \def (arity g c2
 173 TMP_33 a0) in (let TMP_88 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda
 174 (x2: T).(\lambda (H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind
 175 x0) x2))).(let TMP_35 \def (Bind Abbr) in (let TMP_36 \def (CHead d TMP_35 u)
 176 in (let TMP_37 \def (\lambda (c0: C).(getl i c c0)) in (let TMP_38 \def (Bind
 177 x0) in (let TMP_39 \def (CHead x1 TMP_38 x2) in (let TMP_40 \def (Bind Abbr)
 178 in (let TMP_41 \def (CHead d TMP_40 u) in (let TMP_42 \def (Bind x0) in (let
 179 TMP_43 \def (CHead x1 TMP_42 x2) in (let TMP_44 \def (getl_mono c TMP_41 i H0
 180 TMP_43 H11) in (let H12 \def (eq_ind C TMP_36 TMP_37 H0 TMP_39 TMP_44) in
 181 (let TMP_45 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow d |
 182 (CHead c0 _ _) \Rightarrow c0])) in (let TMP_46 \def (Bind Abbr) in (let
 183 TMP_47 \def (CHead d TMP_46 u) in (let TMP_48 \def (Bind x0) in (let TMP_49
 184 \def (CHead x1 TMP_48 x2) in (let TMP_50 \def (Bind Abbr) in (let TMP_51 \def
 185 (CHead d TMP_50 u) in (let TMP_52 \def (Bind x0) in (let TMP_53 \def (CHead
 186 x1 TMP_52 x2) in (let TMP_54 \def (getl_mono c TMP_51 i H0 TMP_53 H11) in
 187 (let H13 \def (f_equal C C TMP_45 TMP_47 TMP_49 TMP_54) in (let TMP_55 \def
 188 (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
 189 \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow
 190 Abbr])])) in (let TMP_56 \def (Bind Abbr) in (let TMP_57 \def (CHead d TMP_56
 191 u) in (let TMP_58 \def (Bind x0) in (let TMP_59 \def (CHead x1 TMP_58 x2) in
 192 (let TMP_60 \def (Bind Abbr) in (let TMP_61 \def (CHead d TMP_60 u) in (let
 193 TMP_62 \def (Bind x0) in (let TMP_63 \def (CHead x1 TMP_62 x2) in (let TMP_64
 194 \def (getl_mono c TMP_61 i H0 TMP_63 H11) in (let H14 \def (f_equal C B
 195 TMP_55 TMP_57 TMP_59 TMP_64) in (let TMP_65 \def (\lambda (e: C).(match e
 196 with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let
 197 TMP_66 \def (Bind Abbr) in (let TMP_67 \def (CHead d TMP_66 u) in (let TMP_68
 198 \def (Bind x0) in (let TMP_69 \def (CHead x1 TMP_68 x2) in (let TMP_70 \def
 199 (Bind Abbr) in (let TMP_71 \def (CHead d TMP_70 u) in (let TMP_72 \def (Bind
 200 x0) in (let TMP_73 \def (CHead x1 TMP_72 x2) in (let TMP_74 \def (getl_mono c
 201 TMP_71 i H0 TMP_73 H11) in (let H15 \def (f_equal C T TMP_65 TMP_67 TMP_69
 202 TMP_74) in (let TMP_86 \def (\lambda (H16: (eq B Abbr x0)).(\lambda (H17: (eq
 203 C d x1)).(let TMP_77 \def (\lambda (t0: T).(let TMP_75 \def (Bind x0) in (let
 204 TMP_76 \def (CHead x1 TMP_75 t0) in (getl i c TMP_76)))) in (let H18 \def
 205 (eq_ind_r T x2 TMP_77 H12 u H15) in (let TMP_80 \def (\lambda (c0: C).(let
 206 TMP_78 \def (Bind x0) in (let TMP_79 \def (CHead c0 TMP_78 u) in (getl i c
 207 TMP_79)))) in (let H19 \def (eq_ind_r C x1 TMP_80 H18 d H17) in (let TMP_81
 208 \def (\lambda (c0: C).(csubv x c0)) in (let H20 \def (eq_ind_r C x1 TMP_81
 209 H10 d H17) in (let TMP_84 \def (\lambda (b: B).(let TMP_82 \def (Bind b) in
 210 (let TMP_83 \def (CHead d TMP_82 u) in (getl i c TMP_83)))) in (let H21 \def
 211 (eq_ind_r B x0 TMP_84 H19 Abbr H16) in (let TMP_85 \def (H2 x H8 H20) in
 212 (arity_abbr g c2 x u i H7 a0 TMP_85)))))))))))) in (let TMP_87 \def (TMP_86
 213 H14) in (TMP_87 H13)))))))))))))))))))))))))))))))))))))))))))))))))))) in
 214 (ex2_3_ind B C T TMP_29 TMP_32 TMP_34 TMP_88 H9))))))))))) in (ex2_ind C
 215 TMP_25 TMP_26 TMP_28 TMP_89 H6))))))) in (let TMP_104 \def (\lambda (H6:
 216 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
 217 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 218 A).(csuba g d2 d)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1:
 219 A).(arity g d2 u2 (asucc g a1))))) (\lambda (_: C).(\lambda (_: T).(\lambda
 220 (a1: A).(arity g d u a1)))))).(let TMP_93 \def (\lambda (d2: C).(\lambda (u2:
 221 T).(\lambda (_: A).(let TMP_91 \def (Bind Abst) in (let TMP_92 \def (CHead d2
 222 TMP_91 u2) in (getl i c2 TMP_92)))))) in (let TMP_94 \def (\lambda (d2:
 223 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d)))) in (let TMP_96 \def
 224 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a1: A).(let TMP_95 \def (asucc g
 225 a1) in (arity g d2 u2 TMP_95))))) in (let TMP_97 \def (\lambda (_:
 226 C).(\lambda (_: T).(\lambda (a1: A).(arity g d u a1)))) in (let TMP_98 \def
 227 (TLRef i) in (let TMP_99 \def (arity g c2 TMP_98 a0) in (let TMP_103 \def
 228 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H7: (getl i c2
 229 (CHead x0 (Bind Abst) x1))).(\lambda (_: (csuba g x0 d)).(\lambda (H9: (arity
 230 g x0 x1 (asucc g x2))).(\lambda (H10: (arity g d u x2)).(let TMP_100 \def
 231 (TLRef i) in (let TMP_101 \def (arity_abst g c2 x0 x1 i H7 x2 H9) in (let
 232 TMP_102 \def (arity_mono g d u x2 H10 a0 H1) in (arity_repl g c2 TMP_100 x2
 233 TMP_101 a0 TMP_102))))))))))) in (ex4_3_ind C T A TMP_93 TMP_94 TMP_96 TMP_97
 234 TMP_99 TMP_103 H6))))))))) in (let TMP_141 \def (\lambda (H6: (ex2_2 C T
 235 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
 236 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))))).(let TMP_107 \def
 237 (\lambda (d2: C).(\lambda (u2: T).(let TMP_105 \def (Bind Void) in (let
 238 TMP_106 \def (CHead d2 TMP_105 u2) in (getl i c2 TMP_106))))) in (let TMP_108
 239 \def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_109 \def
 240 (TLRef i) in (let TMP_110 \def (arity g c2 TMP_109 a0) in (let TMP_140 \def
 241 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H7: (getl i c2 (CHead x0 (Bind
 242 Void) x1))).(\lambda (_: (csuba g x0 d)).(let H_x0 \def (csubv_getl_conf_void
 243 c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in (let TMP_111 \def (\lambda (d2:
 244 C).(\lambda (_: T).(csubv x0 d2))) in (let TMP_114 \def (\lambda (d2:
 245 C).(\lambda (v2: T).(let TMP_112 \def (Bind Void) in (let TMP_113 \def (CHead
 246 d2 TMP_112 v2) in (getl i c TMP_113))))) in (let TMP_115 \def (TLRef i) in
 247 (let TMP_116 \def (arity g c2 TMP_115 a0) in (let TMP_139 \def (\lambda (x2:
 248 C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda (H11: (getl i c
 249 (CHead x2 (Bind Void) x3))).(let TMP_117 \def (Bind Abbr) in (let TMP_118
 250 \def (CHead d TMP_117 u) in (let TMP_119 \def (\lambda (c0: C).(getl i c c0))
 251 in (let TMP_120 \def (Bind Void) in (let TMP_121 \def (CHead x2 TMP_120 x3)
 252 in (let TMP_122 \def (Bind Abbr) in (let TMP_123 \def (CHead d TMP_122 u) in
 253 (let TMP_124 \def (Bind Void) in (let TMP_125 \def (CHead x2 TMP_124 x3) in
 254 (let TMP_126 \def (getl_mono c TMP_123 i H0 TMP_125 H11) in (let H12 \def
 255 (eq_ind C TMP_118 TMP_119 H0 TMP_121 TMP_126) in (let TMP_127 \def (Bind
 256 Abbr) in (let TMP_128 \def (CHead d TMP_127 u) in (let TMP_129 \def (\lambda
 257 (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _)
 258 \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
 259 \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat
 260 _) \Rightarrow False])])) in (let TMP_130 \def (Bind Void) in (let TMP_131
 261 \def (CHead x2 TMP_130 x3) in (let TMP_132 \def (Bind Abbr) in (let TMP_133
 262 \def (CHead d TMP_132 u) in (let TMP_134 \def (Bind Void) in (let TMP_135
 263 \def (CHead x2 TMP_134 x3) in (let TMP_136 \def (getl_mono c TMP_133 i H0
 264 TMP_135 H11) in (let H13 \def (eq_ind C TMP_128 TMP_129 I TMP_131 TMP_136) in
 265 (let TMP_137 \def (TLRef i) in (let TMP_138 \def (arity g c2 TMP_137 a0) in
 266 (False_ind TMP_138 H13))))))))))))))))))))))))))))) in (ex2_2_ind C T TMP_111
 267 TMP_114 TMP_116 TMP_139 H9)))))))))))) in (ex2_2_ind C T TMP_107 TMP_108
 268 TMP_110 TMP_140 H6))))))) in (or3_ind TMP_7 TMP_15 TMP_20 TMP_22 TMP_90
 269 TMP_104 TMP_141 H5)))))))))))))))))))))))))))))) in (let TMP_260 \def
 270 (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
 271 (H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (_: (arity
 272 g d u (asucc g a0))).(\lambda (H2: ((\forall (c2: C).((csuba g c2 d) \to
 273 ((csubv c2 d) \to (arity g c2 u (asucc g a0))))))).(\lambda (c2: C).(\lambda
 274 (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let H_x \def
 275 (csuba_getl_abst_rev g c d u i H0 c2 H3) in (let H5 \def H_x in (let TMP_145
 276 \def (\lambda (d2: C).(let TMP_143 \def (Bind Abst) in (let TMP_144 \def
 277 (CHead d2 TMP_143 u) in (getl i c2 TMP_144)))) in (let TMP_146 \def (\lambda
 278 (d2: C).(csuba g d2 d)) in (let TMP_147 \def (ex2 C TMP_145 TMP_146) in (let
 279 TMP_150 \def (\lambda (d2: C).(\lambda (u2: T).(let TMP_148 \def (Bind Void)
 280 in (let TMP_149 \def (CHead d2 TMP_148 u2) in (getl i c2 TMP_149))))) in (let
 281 TMP_151 \def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let
 282 TMP_152 \def (ex2_2 C T TMP_150 TMP_151) in (let TMP_153 \def (TLRef i) in
 283 (let TMP_154 \def (arity g c2 TMP_153 a0) in (let TMP_222 \def (\lambda (H6:
 284 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
 285 C).(csuba g d2 d)))).(let TMP_157 \def (\lambda (d2: C).(let TMP_155 \def
 286 (Bind Abst) in (let TMP_156 \def (CHead d2 TMP_155 u) in (getl i c2
 287 TMP_156)))) in (let TMP_158 \def (\lambda (d2: C).(csuba g d2 d)) in (let
 288 TMP_159 \def (TLRef i) in (let TMP_160 \def (arity g c2 TMP_159 a0) in (let
 289 TMP_221 \def (\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x (Bind Abst)
 290 u))).(\lambda (H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf c2 c H4
 291 Abst x u i H7) in (let H9 \def H_x0 in (let TMP_161 \def (\lambda (_:
 292 B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2)))) in (let TMP_164 \def
 293 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_162 \def (Bind
 294 b2) in (let TMP_163 \def (CHead d2 TMP_162 v2) in (getl i c TMP_163)))))) in
 295 (let TMP_165 \def (TLRef i) in (let TMP_166 \def (arity g c2 TMP_165 a0) in
 296 (let TMP_220 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda
 297 (H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let
 298 TMP_167 \def (Bind Abst) in (let TMP_168 \def (CHead d TMP_167 u) in (let
 299 TMP_169 \def (\lambda (c0: C).(getl i c c0)) in (let TMP_170 \def (Bind x0)
 300 in (let TMP_171 \def (CHead x1 TMP_170 x2) in (let TMP_172 \def (Bind Abst)
 301 in (let TMP_173 \def (CHead d TMP_172 u) in (let TMP_174 \def (Bind x0) in
 302 (let TMP_175 \def (CHead x1 TMP_174 x2) in (let TMP_176 \def (getl_mono c
 303 TMP_173 i H0 TMP_175 H11) in (let H12 \def (eq_ind C TMP_168 TMP_169 H0
 304 TMP_171 TMP_176) in (let TMP_177 \def (\lambda (e: C).(match e with [(CSort
 305 _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_178 \def
 306 (Bind Abst) in (let TMP_179 \def (CHead d TMP_178 u) in (let TMP_180 \def
 307 (Bind x0) in (let TMP_181 \def (CHead x1 TMP_180 x2) in (let TMP_182 \def
 308 (Bind Abst) in (let TMP_183 \def (CHead d TMP_182 u) in (let TMP_184 \def
 309 (Bind x0) in (let TMP_185 \def (CHead x1 TMP_184 x2) in (let TMP_186 \def
 310 (getl_mono c TMP_183 i H0 TMP_185 H11) in (let H13 \def (f_equal C C TMP_177
 311 TMP_179 TMP_181 TMP_186) in (let TMP_187 \def (\lambda (e: C).(match e with
 312 [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with [(Bind
 313 b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) in (let TMP_188 \def (Bind
 314 Abst) in (let TMP_189 \def (CHead d TMP_188 u) in (let TMP_190 \def (Bind x0)
 315 in (let TMP_191 \def (CHead x1 TMP_190 x2) in (let TMP_192 \def (Bind Abst)
 316 in (let TMP_193 \def (CHead d TMP_192 u) in (let TMP_194 \def (Bind x0) in
 317 (let TMP_195 \def (CHead x1 TMP_194 x2) in (let TMP_196 \def (getl_mono c
 318 TMP_193 i H0 TMP_195 H11) in (let H14 \def (f_equal C B TMP_187 TMP_189
 319 TMP_191 TMP_196) in (let TMP_197 \def (\lambda (e: C).(match e with [(CSort
 320 _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_198 \def
 321 (Bind Abst) in (let TMP_199 \def (CHead d TMP_198 u) in (let TMP_200 \def
 322 (Bind x0) in (let TMP_201 \def (CHead x1 TMP_200 x2) in (let TMP_202 \def
 323 (Bind Abst) in (let TMP_203 \def (CHead d TMP_202 u) in (let TMP_204 \def
 324 (Bind x0) in (let TMP_205 \def (CHead x1 TMP_204 x2) in (let TMP_206 \def
 325 (getl_mono c TMP_203 i H0 TMP_205 H11) in (let H15 \def (f_equal C T TMP_197
 326 TMP_199 TMP_201 TMP_206) in (let TMP_218 \def (\lambda (H16: (eq B Abst
 327 x0)).(\lambda (H17: (eq C d x1)).(let TMP_209 \def (\lambda (t0: T).(let
 328 TMP_207 \def (Bind x0) in (let TMP_208 \def (CHead x1 TMP_207 t0) in (getl i
 329 c TMP_208)))) in (let H18 \def (eq_ind_r T x2 TMP_209 H12 u H15) in (let
 330 TMP_212 \def (\lambda (c0: C).(let TMP_210 \def (Bind x0) in (let TMP_211
 331 \def (CHead c0 TMP_210 u) in (getl i c TMP_211)))) in (let H19 \def (eq_ind_r
 332 C x1 TMP_212 H18 d H17) in (let TMP_213 \def (\lambda (c0: C).(csubv x c0))
 333 in (let H20 \def (eq_ind_r C x1 TMP_213 H10 d H17) in (let TMP_216 \def
 334 (\lambda (b: B).(let TMP_214 \def (Bind b) in (let TMP_215 \def (CHead d
 335 TMP_214 u) in (getl i c TMP_215)))) in (let H21 \def (eq_ind_r B x0 TMP_216
 336 H19 Abst H16) in (let TMP_217 \def (H2 x H8 H20) in (arity_abst g c2 x u i H7
 337 a0 TMP_217)))))))))))) in (let TMP_219 \def (TMP_218 H14) in (TMP_219
 338 H13)))))))))))))))))))))))))))))))))))))))))))))))))))) in (ex2_3_ind B C T
 339 TMP_161 TMP_164 TMP_166 TMP_220 H9))))))))))) in (ex2_ind C TMP_157 TMP_158
 340 TMP_160 TMP_221 H6))))))) in (let TMP_259 \def (\lambda (H6: (ex2_2 C T
 341 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
 342 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))))).(let TMP_225 \def
 343 (\lambda (d2: C).(\lambda (u2: T).(let TMP_223 \def (Bind Void) in (let
 344 TMP_224 \def (CHead d2 TMP_223 u2) in (getl i c2 TMP_224))))) in (let TMP_226
 345 \def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_227 \def
 346 (TLRef i) in (let TMP_228 \def (arity g c2 TMP_227 a0) in (let TMP_258 \def
 347 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H7: (getl i c2 (CHead x0 (Bind
 348 Void) x1))).(\lambda (_: (csuba g x0 d)).(let H_x0 \def (csubv_getl_conf_void
 349 c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in (let TMP_229 \def (\lambda (d2:
 350 C).(\lambda (_: T).(csubv x0 d2))) in (let TMP_232 \def (\lambda (d2:
 351 C).(\lambda (v2: T).(let TMP_230 \def (Bind Void) in (let TMP_231 \def (CHead
 352 d2 TMP_230 v2) in (getl i c TMP_231))))) in (let TMP_233 \def (TLRef i) in
 353 (let TMP_234 \def (arity g c2 TMP_233 a0) in (let TMP_257 \def (\lambda (x2:
 354 C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda (H11: (getl i c
 355 (CHead x2 (Bind Void) x3))).(let TMP_235 \def (Bind Abst) in (let TMP_236
 356 \def (CHead d TMP_235 u) in (let TMP_237 \def (\lambda (c0: C).(getl i c c0))
 357 in (let TMP_238 \def (Bind Void) in (let TMP_239 \def (CHead x2 TMP_238 x3)
 358 in (let TMP_240 \def (Bind Abst) in (let TMP_241 \def (CHead d TMP_240 u) in
 359 (let TMP_242 \def (Bind Void) in (let TMP_243 \def (CHead x2 TMP_242 x3) in
 360 (let TMP_244 \def (getl_mono c TMP_241 i H0 TMP_243 H11) in (let H12 \def
 361 (eq_ind C TMP_236 TMP_237 H0 TMP_239 TMP_244) in (let TMP_245 \def (Bind
 362 Abst) in (let TMP_246 \def (CHead d TMP_245 u) in (let TMP_247 \def (\lambda
 363 (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _)
 364 \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
 365 \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
 366 _) \Rightarrow False])])) in (let TMP_248 \def (Bind Void) in (let TMP_249
 367 \def (CHead x2 TMP_248 x3) in (let TMP_250 \def (Bind Abst) in (let TMP_251
 368 \def (CHead d TMP_250 u) in (let TMP_252 \def (Bind Void) in (let TMP_253
 369 \def (CHead x2 TMP_252 x3) in (let TMP_254 \def (getl_mono c TMP_251 i H0
 370 TMP_253 H11) in (let H13 \def (eq_ind C TMP_246 TMP_247 I TMP_249 TMP_254) in
 371 (let TMP_255 \def (TLRef i) in (let TMP_256 \def (arity g c2 TMP_255 a0) in
 372 (False_ind TMP_256 H13))))))))))))))))))))))))))))) in (ex2_2_ind C T TMP_229
 373 TMP_232 TMP_234 TMP_257 H9)))))))))))) in (ex2_2_ind C T TMP_225 TMP_226
 374 TMP_228 TMP_258 H6))))))) in (or_ind TMP_147 TMP_152 TMP_154 TMP_222 TMP_259
 375 H5)))))))))))))))))))))))) in (let TMP_268 \def (\lambda (b: B).(\lambda (H0:
 376 (not (eq B b Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1:
 377 A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g
 378 c2 c) \to ((csubv c2 c) \to (arity g c2 u a1)))))).(\lambda (t0: T).(\lambda
 379 (a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4:
 380 ((\forall (c2: C).((csuba g c2 (CHead c (Bind b) u)) \to ((csubv c2 (CHead c
 381 (Bind b) u)) \to (arity g c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H5:
 382 (csuba g c2 c)).(\lambda (H6: (csubv c2 c)).(let TMP_261 \def (H2 c2 H5 H6)
 383 in (let TMP_262 \def (Bind b) in (let TMP_263 \def (CHead c2 TMP_262 u) in
 384 (let TMP_264 \def (Bind b) in (let TMP_265 \def (csuba_head g c2 c H5 TMP_264
 385 u) in (let TMP_266 \def (csubv_bind_same c2 c H6 b u u) in (let TMP_267 \def
 386 (H4 TMP_263 TMP_265 TMP_266) in (arity_bind g b H0 c2 u a1 TMP_261 t0 a2
 387 TMP_267)))))))))))))))))))))) in (let TMP_276 \def (\lambda (c: C).(\lambda
 388 (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda
 389 (H1: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 u
 390 (asucc g a1))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g
 391 (CHead c (Bind Abst) u) t0 a2)).(\lambda (H3: ((\forall (c2: C).((csuba g c2
 392 (CHead c (Bind Abst) u)) \to ((csubv c2 (CHead c (Bind Abst) u)) \to (arity g
 393 c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5:
 394 (csubv c2 c)).(let TMP_269 \def (H1 c2 H4 H5) in (let TMP_270 \def (Bind
 395 Abst) in (let TMP_271 \def (CHead c2 TMP_270 u) in (let TMP_272 \def (Bind
 396 Abst) in (let TMP_273 \def (csuba_head g c2 c H4 TMP_272 u) in (let TMP_274
 397 \def (csubv_bind_same c2 c H5 Abst u u) in (let TMP_275 \def (H3 TMP_271
 398 TMP_273 TMP_274) in (arity_head g c2 u a1 TMP_269 t0 a2
 399 TMP_275)))))))))))))))))))) in (let TMP_279 \def (\lambda (c: C).(\lambda (u:
 400 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: ((\forall
 401 (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 u a1)))))).(\lambda
 402 (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda
 403 (H3: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0
 404 (AHead a1 a2))))))).(\lambda (c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda
 405 (H5: (csubv c2 c)).(let TMP_277 \def (H1 c2 H4 H5) in (let TMP_278 \def (H3
 406 c2 H4 H5) in (arity_appl g c2 u a1 TMP_277 t0 a2 TMP_278))))))))))))))) in
 407 (let TMP_282 \def (\lambda (c: C).(\lambda (u: T).(\lambda (a0: A).(\lambda
 408 (_: (arity g c u (asucc g a0))).(\lambda (H1: ((\forall (c2: C).((csuba g c2
 409 c) \to ((csubv c2 c) \to (arity g c2 u (asucc g a0))))))).(\lambda (t0:
 410 T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3: ((\forall (c2: C).((csuba g
 411 c2 c) \to ((csubv c2 c) \to (arity g c2 t0 a0)))))).(\lambda (c2: C).(\lambda
 412 (H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(let TMP_280 \def (H1 c2 H4
 413 H5) in (let TMP_281 \def (H3 c2 H4 H5) in (arity_cast g c2 u a0 TMP_280 t0
 414 TMP_281)))))))))))))) in (let TMP_284 \def (\lambda (c: C).(\lambda (t0:
 415 T).(\lambda (a1: A).(\lambda (_: (arity g c t0 a1)).(\lambda (H1: ((\forall
 416 (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to (arity g c2 t0
 417 a1)))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2:
 418 C).(\lambda (H3: (csuba g c2 c)).(\lambda (H4: (csubv c2 c)).(let TMP_283
 419 \def (H1 c2 H3 H4) in (arity_repl g c2 t0 a1 TMP_283 a2 H2)))))))))))) in
 420 (arity_ind g TMP_1 TMP_2 TMP_142 TMP_260 TMP_268 TMP_276 TMP_279 TMP_282
 421 TMP_284 c1 t a H)))))))))))))).
 422
 423 theorem arity_appls_appl:
 424  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (a1: A).((arity g c
 425 v a1) \to (\forall (u: T).((arity g c u (asucc g a1)) \to (\forall (t:
 426 T).(\forall (vs: TList).(\forall (a2: A).((arity g c (THeads (Flat Appl) vs
 427 (THead (Bind Abbr) v t)) a2) \to (arity g c (THeads (Flat Appl) vs (THead
 428 (Flat Appl) v (THead (Bind Abst) u t))) a2)))))))))))
 429 \def
 430  \lambda (g: G).(\lambda (c: C).(\lambda (v: T).(\lambda (a1: A).(\lambda (H:
 431 (arity g c v a1)).(\lambda (u: T).(\lambda (H0: (arity g c u (asucc g
 432 a1))).(\lambda (t: T).(\lambda (vs: TList).(let TMP_7 \def (\lambda (t0:
 433 TList).(\forall (a2: A).((arity g c (THeads (Flat Appl) t0 (THead (Bind Abbr)
 434 v t)) a2) \to (let TMP_1 \def (Flat Appl) in (let TMP_2 \def (Flat Appl) in
 435 (let TMP_3 \def (Bind Abst) in (let TMP_4 \def (THead TMP_3 u t) in (let
 436 TMP_5 \def (THead TMP_2 v TMP_4) in (let TMP_6 \def (THeads TMP_1 t0 TMP_5)
 437 in (arity g c TMP_6 a2)))))))))) in (let TMP_30 \def (\lambda (a2:
 438 A).(\lambda (H1: (arity g c (THead (Bind Abbr) v t) a2)).(let H_x \def
 439 (arity_gen_bind Abbr not_abbr_abst g c v t a2 H1) in (let H2 \def H_x in (let
 440 TMP_8 \def (\lambda (a3: A).(arity g c v a3)) in (let TMP_11 \def (\lambda
 441 (_: A).(let TMP_9 \def (Bind Abbr) in (let TMP_10 \def (CHead c TMP_9 v) in
 442 (arity g TMP_10 t a2)))) in (let TMP_12 \def (Flat Appl) in (let TMP_13 \def
 443 (Bind Abst) in (let TMP_14 \def (THead TMP_13 u t) in (let TMP_15 \def (THead
 444 TMP_12 v TMP_14) in (let TMP_16 \def (arity g c TMP_15 a2) in (let TMP_29
 445 \def (\lambda (x: A).(\lambda (_: (arity g c v x)).(\lambda (H4: (arity g
 446 (CHead c (Bind Abbr) v) t a2)).(let TMP_17 \def (Bind Abst) in (let TMP_18
 447 \def (THead TMP_17 u t) in (let TMP_19 \def (Bind Abbr) in (let TMP_20 \def
 448 (CHead c TMP_19 v) in (let TMP_21 \def (Bind Abst) in (let TMP_22 \def (CHead
 449 c TMP_21 u) in (let TMP_23 \def (csuba_refl g c) in (let TMP_24 \def
 450 (csuba_abst g c c TMP_23 u a1 H0 v H) in (let TMP_25 \def (csubv_refl c) in
 451 (let TMP_26 \def (csubv_bind c c TMP_25 Abst not_abst_void Abbr u v) in (let
 452 TMP_27 \def (csuba_arity_rev g TMP_20 t a2 H4 TMP_22 TMP_24 TMP_26) in (let
 453 TMP_28 \def (arity_head g c u a1 H0 t a2 TMP_27) in (arity_appl g c v a1 H
 454 TMP_18 a2 TMP_28)))))))))))))))) in (ex2_ind A TMP_8 TMP_11 TMP_16 TMP_29
 455 H2))))))))))))) in (let TMP_60 \def (\lambda (t0: T).(\lambda (t1:
 456 TList).(\lambda (H1: ((\forall (a2: A).((arity g c (THeads (Flat Appl) t1
 457 (THead (Bind Abbr) v t)) a2) \to (arity g c (THeads (Flat Appl) t1 (THead
 458 (Flat Appl) v (THead (Bind Abst) u t))) a2))))).(\lambda (a2: A).(\lambda
 459 (H2: (arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Bind
 460 Abbr) v t))) a2)).(let TMP_31 \def (Flat Appl) in (let TMP_32 \def (Bind
 461 Abbr) in (let TMP_33 \def (THead TMP_32 v t) in (let TMP_34 \def (THeads
 462 TMP_31 t1 TMP_33) in (let H3 \def (arity_gen_appl g c t0 TMP_34 a2 H2) in
 463 (let TMP_35 \def (\lambda (a3: A).(arity g c t0 a3)) in (let TMP_41 \def
 464 (\lambda (a3: A).(let TMP_36 \def (Flat Appl) in (let TMP_37 \def (Bind Abbr)
 465 in (let TMP_38 \def (THead TMP_37 v t) in (let TMP_39 \def (THeads TMP_36 t1
 466 TMP_38) in (let TMP_40 \def (AHead a3 a2) in (arity g c TMP_39 TMP_40)))))))
 467 in (let TMP_42 \def (Flat Appl) in (let TMP_43 \def (Flat Appl) in (let
 468 TMP_44 \def (Flat Appl) in (let TMP_45 \def (Bind Abst) in (let TMP_46 \def
 469 (THead TMP_45 u t) in (let TMP_47 \def (THead TMP_44 v TMP_46) in (let TMP_48
 470 \def (THeads TMP_43 t1 TMP_47) in (let TMP_49 \def (THead TMP_42 t0 TMP_48)
 471 in (let TMP_50 \def (arity g c TMP_49 a2) in (let TMP_59 \def (\lambda (x:
 472 A).(\lambda (H4: (arity g c t0 x)).(\lambda (H5: (arity g c (THeads (Flat
 473 Appl) t1 (THead (Bind Abbr) v t)) (AHead x a2))).(let TMP_51 \def (Flat Appl)
 474 in (let TMP_52 \def (Flat Appl) in (let TMP_53 \def (Bind Abst) in (let
 475 TMP_54 \def (THead TMP_53 u t) in (let TMP_55 \def (THead TMP_52 v TMP_54) in
 476 (let TMP_56 \def (THeads TMP_51 t1 TMP_55) in (let TMP_57 \def (AHead x a2)
 477 in (let TMP_58 \def (H1 TMP_57 H5) in (arity_appl g c t0 x H4 TMP_56 a2
 478 TMP_58)))))))))))) in (ex2_ind A TMP_35 TMP_41 TMP_50 TMP_59
 479 H3))))))))))))))))))))))) in (TList_ind TMP_7 TMP_30 TMP_60 vs)))))))))))).
 480