matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/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
  18
  19 include "csubc/arity.ma".
  20
  21 include "csubc/getl.ma".
  22
  23 include "csubc/drop1.ma".
  24
  25 include "csubc/props.ma".
  26
  27 theorem sc3_arity_csubc:
  28  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1
  29 t a) \to (\forall (d1: C).(\forall (is: PList).((drop1 is d1 c1) \to (\forall
  30 (c2: C).((csubc g d1 c2) \to (sc3 g a c2 (lift1 is t)))))))))))
  31 \def
  32  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
  33 (arity g c1 t a)).(arity_ind g (\lambda (c: C).(\lambda (t0: T).(\lambda (a0:
  34 A).(\forall (d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2:
  35 C).((csubc g d1 c2) \to (sc3 g a0 c2 (lift1 is t0)))))))))) (\lambda (c:
  36 C).(\lambda (n: nat).(\lambda (d1: C).(\lambda (is: PList).(\lambda (_:
  37 (drop1 is d1 c)).(\lambda (c2: C).(\lambda (_: (csubc g d1 c2)).(eq_ind_r T
  38 (TSort n) (\lambda (t0: T).(land (arity g c2 t0 (ASort O n)) (sn3 c2 t0)))
  39 (conj (arity g c2 (TSort n) (ASort O n)) (sn3 c2 (TSort n)) (arity_sort g c2
  40 n) (sn3_nf2 c2 (TSort n) (nf2_sort c2 n))) (lift1 is (TSort n)) (lift1_sort n
  41 is))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i:
  42 nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (a0:
  43 A).(\lambda (_: (arity g d u a0)).(\lambda (H2: ((\forall (d1: C).(\forall
  44 (is: PList).((drop1 is d1 d) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g
  45 a0 c2 (lift1 is u))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda
  46 (H3: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(let
  47 H_x \def (drop1_getl_trans is c d1 H3 Abbr d u i H0) in (let H5 \def H_x in
  48 (ex2_ind C (\lambda (e2: C).(drop1 (ptrans is i) e2 d)) (\lambda (e2:
  49 C).(getl (trans is i) d1 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) u))))
  50 (sc3 g a0 c2 (lift1 is (TLRef i))) (\lambda (x: C).(\lambda (_: (drop1
  51 (ptrans is i) x d)).(\lambda (H7: (getl (trans is i) d1 (CHead x (Bind Abbr)
  52 (lift1 (ptrans is i) u)))).(let H_x0 \def (csubc_getl_conf g d1 (CHead x
  53 (Bind Abbr) (lift1 (ptrans is i) u)) (trans is i) H7 c2 H4) in (let H8 \def
  54 H_x0 in (ex2_ind C (\lambda (e2: C).(getl (trans is i) c2 e2)) (\lambda (e2:
  55 C).(csubc g (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) e2)) (sc3 g a0 c2
  56 (lift1 is (TLRef i))) (\lambda (x0: C).(\lambda (H9: (getl (trans is i) c2
  57 x0)).(\lambda (H10: (csubc g (CHead x (Bind Abbr) (lift1 (ptrans is i) u))
  58 x0)).(let H11 \def (match H10 in csubc return (\lambda (c0: C).(\lambda (c3:
  59 C).(\lambda (_: (csubc ? c0 c3)).((eq C c0 (CHead x (Bind Abbr) (lift1
  60 (ptrans is i) u))) \to ((eq C c3 x0) \to (sc3 g a0 c2 (lift1 is (TLRef
  61 i)))))))) with [(csubc_sort n) \Rightarrow (\lambda (H11: (eq C (CSort n)
  62 (CHead x (Bind Abbr) (lift1 (ptrans is i) u)))).(\lambda (H12: (eq C (CSort
  63 n) x0)).((let H13 \def (eq_ind C (CSort n) (\lambda (e: C).(match e in C
  64 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
  65 \Rightarrow False])) I (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) H11) in
  66 (False_ind ((eq C (CSort n) x0) \to (sc3 g a0 c2 (lift1 is (TLRef i)))) H13))
  67 H12))) | (csubc_head c0 c3 H11 k v) \Rightarrow (\lambda (H12: (eq C (CHead
  68 c0 k v) (CHead x (Bind Abbr) (lift1 (ptrans is i) u)))).(\lambda (H13: (eq C
  69 (CHead c3 k v) x0)).((let H14 \def (f_equal C T (\lambda (e: C).(match e in C
  70 return (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t0)
  71 \Rightarrow t0])) (CHead c0 k v) (CHead x (Bind Abbr) (lift1 (ptrans is i)
  72 u)) H12) in ((let H15 \def (f_equal C K (\lambda (e: C).(match e in C return
  73 (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow
  74 k0])) (CHead c0 k v) (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) H12) in
  75 ((let H16 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
  76 C).C) with [(CSort _) \Rightarrow c0 | (CHead c4 _ _) \Rightarrow c4]))
  77 (CHead c0 k v) (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) H12) in (eq_ind
  78 C x (\lambda (c4: C).((eq K k (Bind Abbr)) \to ((eq T v (lift1 (ptrans is i)
  79 u)) \to ((eq C (CHead c3 k v) x0) \to ((csubc g c4 c3) \to (sc3 g a0 c2
  80 (lift1 is (TLRef i)))))))) (\lambda (H17: (eq K k (Bind Abbr))).(eq_ind K
  81 (Bind Abbr) (\lambda (k0: K).((eq T v (lift1 (ptrans is i) u)) \to ((eq C
  82 (CHead c3 k0 v) x0) \to ((csubc g x c3) \to (sc3 g a0 c2 (lift1 is (TLRef
  83 i))))))) (\lambda (H18: (eq T v (lift1 (ptrans is i) u))).(eq_ind T (lift1
  84 (ptrans is i) u) (\lambda (t0: T).((eq C (CHead c3 (Bind Abbr) t0) x0) \to
  85 ((csubc g x c3) \to (sc3 g a0 c2 (lift1 is (TLRef i)))))) (\lambda (H19: (eq
  86 C (CHead c3 (Bind Abbr) (lift1 (ptrans is i) u)) x0)).(eq_ind C (CHead c3
  87 (Bind Abbr) (lift1 (ptrans is i) u)) (\lambda (_: C).((csubc g x c3) \to (sc3
  88 g a0 c2 (lift1 is (TLRef i))))) (\lambda (_: (csubc g x c3)).(let H21 \def
  89 (eq_ind_r C x0 (\lambda (c4: C).(getl (trans is i) c2 c4)) H9 (CHead c3 (Bind
  90 Abbr) (lift1 (ptrans is i) u)) H19) in (let H_y \def (sc3_abbr g a0 TNil) in
  91 (eq_ind_r T (TLRef (trans is i)) (\lambda (t0: T).(sc3 g a0 c2 t0)) (H_y
  92 (trans is i) c3 (lift1 (ptrans is i) u) c2 (eq_ind T (lift1 is (lift (S i) O
  93 u)) (\lambda (t0: T).(sc3 g a0 c2 t0)) (eq_ind T (lift1 (PConsTail is (S i)
  94 O) u) (\lambda (t0: T).(sc3 g a0 c2 t0)) (H2 d1 (PConsTail is (S i) O)
  95 (drop1_cons_tail c d (S i) O (getl_drop Abbr c d u i H0) is d1 H3) c2 H4)
  96 (lift1 is (lift (S i) O u)) (lift1_cons_tail u (S i) O is)) (lift (S (trans
  97 is i)) O (lift1 (ptrans is i) u)) (lift1_free is i u)) H21) (lift1 is (TLRef
  98 i)) (lift1_lref is i))))) x0 H19)) v (sym_eq T v (lift1 (ptrans is i) u)
  99 H18))) k (sym_eq K k (Bind Abbr) H17))) c0 (sym_eq C c0 x H16))) H15)) H14))
 100 H13 H11))) | (csubc_abst c0 c3 H11 v a1 H12 w H13) \Rightarrow (\lambda (H14:
 101 (eq C (CHead c0 (Bind Abst) v) (CHead x (Bind Abbr) (lift1 (ptrans is i)
 102 u)))).(\lambda (H15: (eq C (CHead c3 (Bind Abbr) w) x0)).((let H16 \def
 103 (eq_ind C (CHead c0 (Bind Abst) v) (\lambda (e: C).(match e in C return
 104 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
 105 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
 106 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
 107 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
 108 \Rightarrow False])])) I (CHead x (Bind Abbr) (lift1 (ptrans is i) u)) H14)
 109 in (False_ind ((eq C (CHead c3 (Bind Abbr) w) x0) \to ((csubc g c0 c3) \to
 110 ((sc3 g (asucc g a1) c0 v) \to ((sc3 g a1 c3 w) \to (sc3 g a0 c2 (lift1 is
 111 (TLRef i))))))) H16)) H15 H11 H12 H13)))]) in (H11 (refl_equal C (CHead x
 112 (Bind Abbr) (lift1 (ptrans is i) u))) (refl_equal C x0)))))) H8))))))
 113 H5)))))))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda
 114 (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0:
 115 A).(\lambda (H1: (arity g d u (asucc g a0))).(\lambda (_: ((\forall (d1:
 116 C).(\forall (is: PList).((drop1 is d1 d) \to (\forall (c2: C).((csubc g d1
 117 c2) \to (sc3 g (asucc g a0) c2 (lift1 is u))))))))).(\lambda (d1: C).(\lambda
 118 (is: PList).(\lambda (H3: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H4:
 119 (csubc g d1 c2)).(let H5 \def H0 in (let H_x \def (drop1_getl_trans is c d1
 120 H3 Abst d u i H5) in (let H6 \def H_x in (ex2_ind C (\lambda (e2: C).(drop1
 121 (ptrans is i) e2 d)) (\lambda (e2: C).(getl (trans is i) d1 (CHead e2 (Bind
 122 Abst) (lift1 (ptrans is i) u)))) (sc3 g a0 c2 (lift1 is (TLRef i))) (\lambda
 123 (x: C).(\lambda (H7: (drop1 (ptrans is i) x d)).(\lambda (H8: (getl (trans is
 124 i) d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)))).(let H_x0 \def
 125 (csubc_getl_conf g d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)) (trans is
 126 i) H8 c2 H4) in (let H9 \def H_x0 in (ex2_ind C (\lambda (e2: C).(getl (trans
 127 is i) c2 e2)) (\lambda (e2: C).(csubc g (CHead x (Bind Abst) (lift1 (ptrans
 128 is i) u)) e2)) (sc3 g a0 c2 (lift1 is (TLRef i))) (\lambda (x0: C).(\lambda
 129 (H10: (getl (trans is i) c2 x0)).(\lambda (H11: (csubc g (CHead x (Bind Abst)
 130 (lift1 (ptrans is i) u)) x0)).(let H12 \def (match H11 in csubc return
 131 (\lambda (c0: C).(\lambda (c3: C).(\lambda (_: (csubc ? c0 c3)).((eq C c0
 132 (CHead x (Bind Abst) (lift1 (ptrans is i) u))) \to ((eq C c3 x0) \to (sc3 g
 133 a0 c2 (lift1 is (TLRef i)))))))) with [(csubc_sort n) \Rightarrow (\lambda
 134 (H12: (eq C (CSort n) (CHead x (Bind Abst) (lift1 (ptrans is i)
 135 u)))).(\lambda (H13: (eq C (CSort n) x0)).((let H14 \def (eq_ind C (CSort n)
 136 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
 137 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead x (Bind Abst)
 138 (lift1 (ptrans is i) u)) H12) in (False_ind ((eq C (CSort n) x0) \to (sc3 g
 139 a0 c2 (lift1 is (TLRef i)))) H14)) H13))) | (csubc_head c0 c3 H12 k v)
 140 \Rightarrow (\lambda (H13: (eq C (CHead c0 k v) (CHead x (Bind Abst) (lift1
 141 (ptrans is i) u)))).(\lambda (H14: (eq C (CHead c3 k v) x0)).((let H15 \def
 142 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 143 [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k v)
 144 (CHead x (Bind Abst) (lift1 (ptrans is i) u)) H13) in ((let H16 \def (f_equal
 145 C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
 146 \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k v) (CHead x
 147 (Bind Abst) (lift1 (ptrans is i) u)) H13) in ((let H17 \def (f_equal C C
 148 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 149 \Rightarrow c0 | (CHead c4 _ _) \Rightarrow c4])) (CHead c0 k v) (CHead x
 150 (Bind Abst) (lift1 (ptrans is i) u)) H13) in (eq_ind C x (\lambda (c4:
 151 C).((eq K k (Bind Abst)) \to ((eq T v (lift1 (ptrans is i) u)) \to ((eq C
 152 (CHead c3 k v) x0) \to ((csubc g c4 c3) \to (sc3 g a0 c2 (lift1 is (TLRef
 153 i)))))))) (\lambda (H18: (eq K k (Bind Abst))).(eq_ind K (Bind Abst) (\lambda
 154 (k0: K).((eq T v (lift1 (ptrans is i) u)) \to ((eq C (CHead c3 k0 v) x0) \to
 155 ((csubc g x c3) \to (sc3 g a0 c2 (lift1 is (TLRef i))))))) (\lambda (H19: (eq
 156 T v (lift1 (ptrans is i) u))).(eq_ind T (lift1 (ptrans is i) u) (\lambda (t0:
 157 T).((eq C (CHead c3 (Bind Abst) t0) x0) \to ((csubc g x c3) \to (sc3 g a0 c2
 158 (lift1 is (TLRef i)))))) (\lambda (H20: (eq C (CHead c3 (Bind Abst) (lift1
 159 (ptrans is i) u)) x0)).(eq_ind C (CHead c3 (Bind Abst) (lift1 (ptrans is i)
 160 u)) (\lambda (_: C).((csubc g x c3) \to (sc3 g a0 c2 (lift1 is (TLRef i)))))
 161 (\lambda (_: (csubc g x c3)).(let H22 \def (eq_ind_r C x0 (\lambda (c4:
 162 C).(getl (trans is i) c2 c4)) H10 (CHead c3 (Bind Abst) (lift1 (ptrans is i)
 163 u)) H20) in (let H_y \def (sc3_abst g a0 TNil) in (eq_ind_r T (TLRef (trans
 164 is i)) (\lambda (t0: T).(sc3 g a0 c2 t0)) (H_y c2 (trans is i)
 165 (csubc_arity_conf g d1 c2 H4 (TLRef (trans is i)) a0 (eq_ind T (lift1 is
 166 (TLRef i)) (\lambda (t0: T).(arity g d1 t0 a0)) (arity_lift1 g a0 c is d1
 167 (TLRef i) H3 (arity_abst g c d u i H0 a0 H1)) (TLRef (trans is i))
 168 (lift1_lref is i))) (nf2_lref_abst c2 c3 (lift1 (ptrans is i) u) (trans is i)
 169 H22) I) (lift1 is (TLRef i)) (lift1_lref is i))))) x0 H20)) v (sym_eq T v
 170 (lift1 (ptrans is i) u) H19))) k (sym_eq K k (Bind Abst) H18))) c0 (sym_eq C
 171 c0 x H17))) H16)) H15)) H14 H12))) | (csubc_abst c0 c3 H12 v a1 H13 w H14)
 172 \Rightarrow (\lambda (H15: (eq C (CHead c0 (Bind Abst) v) (CHead x (Bind
 173 Abst) (lift1 (ptrans is i) u)))).(\lambda (H16: (eq C (CHead c3 (Bind Abbr)
 174 w) x0)).((let H17 \def (f_equal C T (\lambda (e: C).(match e in C return
 175 (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow
 176 t0])) (CHead c0 (Bind Abst) v) (CHead x (Bind Abst) (lift1 (ptrans is i) u))
 177 H15) in ((let H18 \def (f_equal C C (\lambda (e: C).(match e in C return
 178 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c4 _ _)
 179 \Rightarrow c4])) (CHead c0 (Bind Abst) v) (CHead x (Bind Abst) (lift1
 180 (ptrans is i) u)) H15) in (eq_ind C x (\lambda (c4: C).((eq T v (lift1
 181 (ptrans is i) u)) \to ((eq C (CHead c3 (Bind Abbr) w) x0) \to ((csubc g c4
 182 c3) \to ((sc3 g (asucc g a1) c4 v) \to ((sc3 g a1 c3 w) \to (sc3 g a0 c2
 183 (lift1 is (TLRef i))))))))) (\lambda (H19: (eq T v (lift1 (ptrans is i)
 184 u))).(eq_ind T (lift1 (ptrans is i) u) (\lambda (t0: T).((eq C (CHead c3
 185 (Bind Abbr) w) x0) \to ((csubc g x c3) \to ((sc3 g (asucc g a1) x t0) \to
 186 ((sc3 g a1 c3 w) \to (sc3 g a0 c2 (lift1 is (TLRef i)))))))) (\lambda (H20:
 187 (eq C (CHead c3 (Bind Abbr) w) x0)).(eq_ind C (CHead c3 (Bind Abbr) w)
 188 (\lambda (_: C).((csubc g x c3) \to ((sc3 g (asucc g a1) x (lift1 (ptrans is
 189 i) u)) \to ((sc3 g a1 c3 w) \to (sc3 g a0 c2 (lift1 is (TLRef i)))))))
 190 (\lambda (_: (csubc g x c3)).(\lambda (H22: (sc3 g (asucc g a1) x (lift1
 191 (ptrans is i) u))).(\lambda (H23: (sc3 g a1 c3 w)).(let H24 \def (eq_ind_r C
 192 x0 (\lambda (c4: C).(getl (trans is i) c2 c4)) H10 (CHead c3 (Bind Abbr) w)
 193 H20) in (let H_y \def (sc3_abbr g a0 TNil) in (eq_ind_r T (TLRef (trans is
 194 i)) (\lambda (t0: T).(sc3 g a0 c2 t0)) (H_y (trans is i) c3 w c2 (let H_y0
 195 \def (arity_lift1 g (asucc g a0) d (ptrans is i) x u H7 H1) in (let H_y1 \def
 196 (sc3_arity_gen g x (lift1 (ptrans is i) u) (asucc g a1) H22) in (sc3_repl g
 197 a1 c2 (lift (S (trans is i)) O w) (sc3_lift g a1 c3 w H23 c2 (S (trans is i))
 198 O (getl_drop Abbr c2 c3 w (trans is i) H24)) a0 (asucc_inj g a1 a0
 199 (arity_mono g x (lift1 (ptrans is i) u) (asucc g a1) H_y1 (asucc g a0)
 200 H_y0))))) H24) (lift1 is (TLRef i)) (lift1_lref is i))))))) x0 H20)) v
 201 (sym_eq T v (lift1 (ptrans is i) u) H19))) c0 (sym_eq C c0 x H18))) H17)) H16
 202 H12 H13 H14)))]) in (H12 (refl_equal C (CHead x (Bind Abst) (lift1 (ptrans is
 203 i) u))) (refl_equal C x0)))))) H9)))))) H6))))))))))))))))) (\lambda (b:
 204 B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda (u:
 205 T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall
 206 (d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g
 207 d1 c2) \to (sc3 g a1 c2 (lift1 is u))))))))).(\lambda (t0: T).(\lambda (a2:
 208 A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: ((\forall
 209 (d1: C).(\forall (is: PList).((drop1 is d1 (CHead c (Bind b) u)) \to (\forall
 210 (c2: C).((csubc g d1 c2) \to (sc3 g a2 c2 (lift1 is t0))))))))).(\lambda (d1:
 211 C).(\lambda (is: PList).(\lambda (H5: (drop1 is d1 c)).(\lambda (c2:
 212 C).(\lambda (H6: (csubc g d1 c2)).(let H_y \def (sc3_bind g b H0 a1 a2 TNil)
 213 in (eq_ind_r T (THead (Bind b) (lift1 is u) (lift1 (Ss is) t0)) (\lambda (t1:
 214 T).(sc3 g a2 c2 t1)) (H_y c2 (lift1 is u) (lift1 (Ss is) t0) (H4 (CHead d1
 215 (Bind b) (lift1 is u)) (Ss is) (drop1_skip_bind b c is d1 u H5) (CHead c2
 216 (Bind b) (lift1 is u)) (csubc_head g d1 c2 H6 (Bind b) (lift1 is u))) (H2 d1
 217 is H5 c2 H6)) (lift1 is (THead (Bind b) u t0)) (lift1_bind b is u
 218 t0))))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1:
 219 A).(\lambda (H0: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (d1:
 220 C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1
 221 c2) \to (sc3 g (asucc g a1) c2 (lift1 is u))))))))).(\lambda (t0: T).(\lambda
 222 (a2: A).(\lambda (H2: (arity g (CHead c (Bind Abst) u) t0 a2)).(\lambda (H3:
 223 ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 (CHead c (Bind Abst) u))
 224 \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a2 c2 (lift1 is
 225 t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H4: (drop1 is d1
 226 c)).(\lambda (c2: C).(\lambda (H5: (csubc g d1 c2)).(eq_ind_r T (THead (Bind
 227 Abst) (lift1 is u) (lift1 (Ss is) t0)) (\lambda (t1: T).(land (arity g c2 t1
 228 (AHead a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall
 229 (is0: PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1
 230 is0 t1)))))))))) (conj (arity g c2 (THead (Bind Abst) (lift1 is u) (lift1 (Ss
 231 is) t0)) (AHead a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to
 232 (\forall (is0: PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat Appl) w
 233 (lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0))))))))))
 234 (csubc_arity_conf g d1 c2 H5 (THead (Bind Abst) (lift1 is u) (lift1 (Ss is)
 235 t0)) (AHead a1 a2) (arity_head g d1 (lift1 is u) a1 (arity_lift1 g (asucc g
 236 a1) c is d1 u H4 H0) (lift1 (Ss is) t0) a2 (arity_lift1 g a2 (CHead c (Bind
 237 Abst) u) (Ss is) (CHead d1 (Bind Abst) (lift1 is u)) t0 (drop1_skip_bind Abst
 238 c is d1 u H4) H2))) (\lambda (d: C).(\lambda (w: T).(\lambda (H6: (sc3 g a1 d
 239 w)).(\lambda (is0: PList).(\lambda (H7: (drop1 is0 d c2)).(eq_ind_r T (THead
 240 (Bind Abst) (lift1 is0 (lift1 is u)) (lift1 (Ss is0) (lift1 (Ss is) t0)))
 241 (\lambda (t1: T).(sc3 g a2 d (THead (Flat Appl) w t1))) (let H8 \def
 242 (sc3_appl g a1 a2 TNil) in (H8 d w (lift1 (Ss is0) (lift1 (Ss is) t0)) (let
 243 H_y \def (sc3_bind g Abbr (\lambda (H9: (eq B Abbr Abst)).(not_abbr_abst H9))
 244 a1 a2 TNil) in (H_y d w (lift1 (Ss is0) (lift1 (Ss is) t0)) (let H_x \def
 245 (csubc_drop1_conf_rev g is0 d c2 H7 d1 H5) in (let H9 \def H_x in (ex2_ind C
 246 (\lambda (c3: C).(drop1 is0 c3 d1)) (\lambda (c3: C).(csubc g c3 d)) (sc3 g
 247 a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0))) (\lambda (x:
 248 C).(\lambda (H10: (drop1 is0 x d1)).(\lambda (H11: (csubc g x d)).(eq_ind_r T
 249 (lift1 (papp (Ss is0) (Ss is)) t0) (\lambda (t1: T).(sc3 g a2 (CHead d (Bind
 250 Abbr) w) t1)) (eq_ind_r PList (Ss (papp is0 is)) (\lambda (p: PList).(sc3 g
 251 a2 (CHead d (Bind Abbr) w) (lift1 p t0))) (H3 (CHead x (Bind Abst) (lift1
 252 (papp is0 is) u)) (Ss (papp is0 is)) (drop1_skip_bind Abst c (papp is0 is) x
 253 u (drop1_trans is0 x d1 H10 is c H4)) (CHead d (Bind Abbr) w) (csubc_abst g x
 254 d H11 (lift1 (papp is0 is) u) a1 (H1 x (papp is0 is) (drop1_trans is0 x d1
 255 H10 is c H4) x (csubc_refl g x)) w H6)) (papp (Ss is0) (Ss is)) (papp_ss is0
 256 is)) (lift1 (Ss is0) (lift1 (Ss is) t0)) (lift1_lift1 (Ss is0) (Ss is)
 257 t0))))) H9))) H6)) H6 (lift1 is0 (lift1 is u)) (sc3_lift1 g c2 (asucc g a1)
 258 is0 d (lift1 is u) (H1 d1 is H4 c2 H5) H7))) (lift1 is0 (THead (Bind Abst)
 259 (lift1 is u) (lift1 (Ss is) t0))) (lift1_bind Abst is0 (lift1 is u) (lift1
 260 (Ss is) t0))))))))) (lift1 is (THead (Bind Abst) u t0)) (lift1_bind Abst is u
 261 t0)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda
 262 (_: (arity g c u a1)).(\lambda (H1: ((\forall (d1: C).(\forall (is:
 263 PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a1
 264 c2 (lift1 is u))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity
 265 g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (d1: C).(\forall (is:
 266 PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g
 267 (AHead a1 a2) c2 (lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is:
 268 PList).(\lambda (H4: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H5: (csubc g
 269 d1 c2)).(let H_y \def (H1 d1 is H4 c2 H5) in (let H_y0 \def (H3 d1 is H4 c2
 270 H5) in (let H6 \def H_y0 in (and_ind (arity g c2 (lift1 is t0) (AHead a1 a2))
 271 (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0:
 272 PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0
 273 (lift1 is t0))))))))) (sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0)))
 274 (\lambda (_: (arity g c2 (lift1 is t0) (AHead a1 a2))).(\lambda (H8:
 275 ((\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0:
 276 PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0
 277 (lift1 is t0))))))))))).(let H_y1 \def (H8 c2 (lift1 is u) H_y PNil) in
 278 (eq_ind_r T (THead (Flat Appl) (lift1 is u) (lift1 is t0)) (\lambda (t1:
 279 T).(sc3 g a2 c2 t1)) (H_y1 (drop1_nil c2)) (lift1 is (THead (Flat Appl) u
 280 t0)) (lift1_flat Appl is u t0))))) H6)))))))))))))))))) (\lambda (c:
 281 C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g
 282 a0))).(\lambda (H1: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c)
 283 \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g (asucc g a0) c2 (lift1 is
 284 u))))))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3:
 285 ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2:
 286 C).((csubc g d1 c2) \to (sc3 g a0 c2 (lift1 is t0))))))))).(\lambda (d1:
 287 C).(\lambda (is: PList).(\lambda (H4: (drop1 is d1 c)).(\lambda (c2:
 288 C).(\lambda (H5: (csubc g d1 c2)).(let H_y \def (sc3_cast g a0 TNil) in
 289 (eq_ind_r T (THead (Flat Cast) (lift1 is u) (lift1 is t0)) (\lambda (t1:
 290 T).(sc3 g a0 c2 t1)) (H_y c2 (lift1 is u) (H1 d1 is H4 c2 H5) (lift1 is t0)
 291 (H3 d1 is H4 c2 H5)) (lift1 is (THead (Flat Cast) u t0)) (lift1_flat Cast is
 292 u t0)))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1:
 293 A).(\lambda (_: (arity g c t0 a1)).(\lambda (H1: ((\forall (d1: C).(\forall
 294 (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g
 295 a1 c2 (lift1 is t0))))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1
 296 a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is d1
 297 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2 (lift1
 298 is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).
 299
 300 theorem sc3_arity:
 301  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
 302 a) \to (sc3 g a c t)))))
 303 \def
 304  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
 305 (arity g c t a)).(let H_y \def (sc3_arity_csubc g c t a H c PNil) in (H_y
 306 (drop1_nil c) c (csubc_refl g c))))))).
 307