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