helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl".
  18
  19 include "clen/defs.ma".
  20
  21 include "getl/props.ma".
  22
  23 theorem getl_ctail_clen:
  24  \forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n:
  25 nat).(getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t))))))
  26 \def
  27  \lambda (b: B).(\lambda (t: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(ex
  28 nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort n)
  29 (Bind b) t))))) (\lambda (n: nat).(ex_intro nat (\lambda (n0: nat).(getl O
  30 (CHead (CSort n) (Bind b) t) (CHead (CSort n0) (Bind b) t))) n (getl_refl b
  31 (CSort n) t))) (\lambda (c0: C).(\lambda (H: (ex nat (\lambda (n: nat).(getl
  32 (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))))).(\lambda (k:
  33 K).(\lambda (t0: T).(let H0 \def H in (ex_ind nat (\lambda (n: nat).(getl
  34 (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))) (ex nat
  35 (\lambda (n: nat).(getl (s k (clen c0)) (CHead (CTail (Bind b) t c0) k t0)
  36 (CHead (CSort n) (Bind b) t)))) (\lambda (x: nat).(\lambda (H1: (getl (clen
  37 c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t))).(match k in K return
  38 (\lambda (k0: K).(ex nat (\lambda (n: nat).(getl (s k0 (clen c0)) (CHead
  39 (CTail (Bind b) t c0) k0 t0) (CHead (CSort n) (Bind b) t))))) with [(Bind b0)
  40 \Rightarrow (ex_intro nat (\lambda (n: nat).(getl (S (clen c0)) (CHead (CTail
  41 (Bind b) t c0) (Bind b0) t0) (CHead (CSort n) (Bind b) t))) x (getl_head
  42 (Bind b0) (clen c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t) H1
  43 t0)) | (Flat f) \Rightarrow (ex_intro nat (\lambda (n: nat).(getl (clen c0)
  44 (CHead (CTail (Bind b) t c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x
  45 (getl_flat (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f
  46 t0))]))) H0)))))) c))).
  47
  48 theorem getl_gen_tail:
  49  \forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall
  50 (c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2
  51 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
  52 (\lambda (e: C).(getl i c1 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
  53 nat).(eq nat i (clen c1))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
  54 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))))))
  55 \def
  56  \lambda (k: K).(\lambda (b: B).(\lambda (u1: T).(\lambda (u2: T).(\lambda
  57 (c2: C).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (i: nat).((getl i
  58 (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C
  59 c2 (CTail k u1 e))) (\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4
  60 nat (\lambda (_: nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind
  61 b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort
  62 n)))))))) (\lambda (n: nat).(\lambda (i: nat).(match i in nat return (\lambda
  63 (n0: nat).((getl n0 (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)) \to (or
  64 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n0
  65 (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0
  66 (clen (CSort n)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq
  67 T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort n1))))))) with [O \Rightarrow
  68 (\lambda (H: (getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2))).((match
  69 k in K return (\lambda (k0: K).((clear (CHead (CSort n) k0 u1) (CHead c2
  70 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k0 u1 e)))
  71 (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda
  72 (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K k0 (Bind b))) (\lambda (_:
  73 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))))) with [(Bind
  74 b0) \Rightarrow (\lambda (H0: (clear (CHead (CSort n) (Bind b0) u1) (CHead c2
  75 (Bind b) u2))).(let H1 \def (f_equal C C (\lambda (e: C).(match e in C return
  76 (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow
  77 c])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1) (clear_gen_bind b0
  78 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in ((let H2 \def (f_equal C B
  79 (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
  80 \Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_:
  81 K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2
  82 (Bind b) u2) (CHead (CSort n) (Bind b0) u1) (clear_gen_bind b0 (CSort n)
  83 (CHead c2 (Bind b) u2) u1 H0)) in ((let H3 \def (f_equal C T (\lambda (e:
  84 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 |
  85 (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind
  86 b0) u1) (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in
  87 (\lambda (H4: (eq B b b0)).(\lambda (H5: (eq C c2 (CSort n))).(eq_ind_r C
  88 (CSort n) (\lambda (c: C).(or (ex2 C (\lambda (e: C).(eq C c (CTail (Bind b0)
  89 u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat
  90 (\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b)))
  91 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c (CSort n0))))))
  92 (eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (e: C).(eq C (CSort n)
  93 (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b)
  94 t)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind
  95 b0) (Bind b))) (\lambda (_: nat).(eq T u1 t)) (\lambda (n0: nat).(eq C (CSort
  96 n) (CSort n0)))))) (eq_ind_r B b0 (\lambda (b1: B).(or (ex2 C (\lambda (e:
  97 C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n)
  98 (CHead e (Bind b1) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda
  99 (_: nat).(eq K (Bind b0) (Bind b1))) (\lambda (_: nat).(eq T u1 u1)) (\lambda
 100 (n0: nat).(eq C (CSort n) (CSort n0)))))) (or_intror (ex2 C (\lambda (e:
 101 C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O (CSort n)
 102 (CHead e (Bind b0) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda
 103 (_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq T u1 u1)) (\lambda
 104 (n0: nat).(eq C (CSort n) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq
 105 nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b0))) (\lambda (_: nat).(eq
 106 T u1 u1)) (\lambda (n0: nat).(eq C (CSort n) (CSort n0))) n (refl_equal nat
 107 O) (refl_equal K (Bind b0)) (refl_equal T u1) (refl_equal C (CSort n)))) b
 108 H4) u2 H3) c2 H5)))) H2)) H1))) | (Flat f) \Rightarrow (\lambda (H0: (clear
 109 (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2))).(clear_gen_sort (CHead
 110 c2 (Bind b) u2) n (clear_gen_flat f (CSort n) (CHead c2 (Bind b) u2) u1 H0)
 111 (or (ex2 C (\lambda (e: C).(eq C c2 (CTail (Flat f) u1 e))) (\lambda (e:
 112 C).(getl O (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
 113 nat O O)) (\lambda (_: nat).(eq K (Flat f) (Bind b))) (\lambda (_: nat).(eq T
 114 u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))))))]) (getl_gen_O (CHead
 115 (CSort n) k u1) (CHead c2 (Bind b) u2) H))) | (S n0) \Rightarrow (\lambda (H:
 116 (getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2))).(getl_gen_sort n
 117 (r k n0) (CHead c2 (Bind b) u2) (getl_gen_S k (CSort n) (CHead c2 (Bind b)
 118 u2) u1 n0 H) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda
 119 (e: C).(getl (S n0) (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
 120 nat).(eq nat (S n0) O)) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 121 nat).(eq T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort n1)))))))]))) (\lambda
 122 (c: C).(\lambda (H: ((\forall (i: nat).((getl i (CTail k u1 c) (CHead c2
 123 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
 124 (\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
 125 nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 126 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))).(\lambda (k0:
 127 K).(\lambda (t: T).(\lambda (i: nat).(match i in nat return (\lambda (n:
 128 nat).((getl n (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)) \to (or
 129 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n
 130 (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n
 131 (clen (CHead c k0 t)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 132 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))))) with [O
 133 \Rightarrow (\lambda (H0: (getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind
 134 b) u2))).((match k0 in K return (\lambda (k1: K).((clear (CHead (CTail k u1
 135 c) k1 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2
 136 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c k1 t) (CHead e (Bind b)
 137 u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s k1 (clen c)))) (\lambda (_:
 138 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
 139 C c2 (CSort n))))))) with [(Bind b0) \Rightarrow (\lambda (H1: (clear (CHead
 140 (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2))).(let H2 \def (f_equal C
 141 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 142 \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 (Bind b) u2) (CHead
 143 (CTail k u1 c) (Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind
 144 b) u2) t H1)) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in C
 145 return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _)
 146 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
 147 \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead
 148 (CTail k u1 c) (Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind
 149 b) u2) t H1)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e in C
 150 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 | (CHead _ _ t)
 151 \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
 152 (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) in (\lambda
 153 (H5: (eq B b b0)).(\lambda (H6: (eq C c2 (CTail k u1 c))).(eq_ind T u2
 154 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
 155 (\lambda (e: C).(getl O (CHead c (Bind b0) t0) (CHead e (Bind b) u2)))) (ex4
 156 nat (\lambda (_: nat).(eq nat O (s (Bind b0) (clen c)))) (\lambda (_:
 157 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
 158 C c2 (CSort n)))))) (eq_ind B b (\lambda (b1: B).(or (ex2 C (\lambda (e:
 159 C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b1) u2)
 160 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b1)
 161 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 162 u2)) (\lambda (n: nat).(eq C c2 (CSort n)))))) (let H7 \def (eq_ind C c2
 163 (\lambda (c0: C).(\forall (i: nat).((getl i (CTail k u1 c) (CHead c0 (Bind b)
 164 u2)) \to (or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e:
 165 C).(getl i c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat i
 166 (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 167 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))))) H (CTail k u1 c) H6) in
 168 (eq_ind_r C (CTail k u1 c) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C
 169 c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) (CHead e
 170 (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b) (clen c))))
 171 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
 172 (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e: C).(eq C
 173 (CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2)
 174 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b)
 175 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 176 u2)) (\lambda (n: nat).(eq C (CTail k u1 c) (CSort n)))) (ex_intro2 C
 177 (\lambda (e: C).(eq C (CTail k u1 c) (CTail k u1 e))) (\lambda (e: C).(getl O
 178 (CHead c (Bind b) u2) (CHead e (Bind b) u2))) c (refl_equal C (CTail k u1 c))
 179 (getl_refl b c u2))) c2 H6)) b0 H5) t H4)))) H3)) H2))) | (Flat f)
 180 \Rightarrow (\lambda (H1: (clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2
 181 (Bind b) u2))).(let H2 \def (H O (getl_intro O (CTail k u1 c) (CHead c2 (Bind
 182 b) u2) (CTail k u1 c) (drop_refl (CTail k u1 c)) (clear_gen_flat f (CTail k
 183 u1 c) (CHead c2 (Bind b) u2) t H1))) in (or_ind (ex2 C (\lambda (e: C).(eq C
 184 c2 (CTail k u1 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2)))) (ex4
 185 nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind
 186 b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))
 187 (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O
 188 (CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
 189 nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda
 190 (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (H3:
 191 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O c
 192 (CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1
 193 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2))) (or (ex2 C (\lambda
 194 (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
 195 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
 196 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 197 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (x: C).(\lambda (H4:
 198 (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x (Bind b)
 199 u2))).(eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e:
 200 C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
 201 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
 202 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 203 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e:
 204 C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
 205 (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
 206 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 207 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C (CTail k u1 x) (CSort n))))
 208 (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda
 209 (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))) x (refl_equal C
 210 (CTail k u1 x)) (getl_flat c (CHead x (Bind b) u2) O H5 f t))) c2 H4)))) H3))
 211 (\lambda (H3: (ex4 nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_:
 212 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
 213 C c2 (CSort n))))).(ex4_ind nat (\lambda (_: nat).(eq nat O (clen c)))
 214 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
 215 (n: nat).(eq C c2 (CSort n))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
 216 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))))
 217 (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_:
 218 nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
 219 C c2 (CSort n))))) (\lambda (x0: nat).(\lambda (H4: (eq nat O (clen
 220 c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda
 221 (H7: (eq C c2 (CSort x0))).(eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C
 222 (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
 223 (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
 224 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 225 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (eq_ind T u1
 226 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k u1 e)))
 227 (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) t0)))) (ex4
 228 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
 229 K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n: nat).(eq C (CSort
 230 x0) (CSort n)))))) (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda
 231 (e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl O (CHead c
 232 (Flat f) t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
 233 (Flat f) (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_:
 234 nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))))))
 235 (or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e)))
 236 (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)))) (ex4
 237 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
 238 K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n: nat).(eq C
 239 (CSort x0) (CSort n)))) (ex4_intro nat (\lambda (_: nat).(eq nat O (s (Flat
 240 f) (clen c)))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_:
 241 nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))) x0 H4
 242 (refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) k H5)
 243 u2 H6) c2 H7)))))) H3)) H2)))]) (getl_gen_O (CHead (CTail k u1 c) k0 t)
 244 (CHead c2 (Bind b) u2) H0))) | (S n) \Rightarrow (\lambda (H0: (getl (S n)
 245 (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let H_x \def (H (r k0
 246 n) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H0)) in (let H1
 247 \def H_x in (or_ind (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda
 248 (e: C).(getl (r k0 n) c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
 249 nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b)))
 250 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))) (or
 251 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n)
 252 (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S
 253 n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 254 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (H2:
 255 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0
 256 n) c (CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k
 257 u1 e))) (\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))) (or (ex2 C
 258 (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
 259 c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
 260 k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
 261 u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x: C).(\lambda
 262 (H3: (eq C c2 (CTail k u1 x))).(\lambda (H4: (getl (r k0 n) c (CHead x (Bind
 263 b) u2))).(let H5 \def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k
 264 u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind
 265 b) u2) t n H0) (CTail k u1 x) H3) in (eq_ind_r C (CTail k u1 x) (\lambda (c0:
 266 C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl
 267 (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
 268 nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 269 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0)))))) (or_introl
 270 (ex2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e:
 271 C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_:
 272 nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b)))
 273 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C (CTail k u1 x)
 274 (CSort n0)))) (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1
 275 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2))) x
 276 (refl_equal C (CTail k u1 x)) (getl_head k0 n c (CHead x (Bind b) u2) H4 t)))
 277 c2 H3))))) H2)) (\lambda (H2: (ex4 nat (\lambda (_: nat).(eq nat (r k0 n)
 278 (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
 279 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))).(ex4_ind nat (\lambda (_:
 280 nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b)))
 281 (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))) (or
 282 (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n)
 283 (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S
 284 n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 285 nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x0:
 286 nat).(\lambda (H3: (eq nat (r k0 n) (clen c))).(\lambda (H4: (eq K k (Bind
 287 b))).(\lambda (H5: (eq T u1 u2)).(\lambda (H6: (eq C c2 (CSort x0))).(let H7
 288 \def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k u1 c) (CHead c0
 289 (Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H0)
 290 (CSort x0) H6) in (eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C (\lambda
 291 (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t)
 292 (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen
 293 c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2))
 294 (\lambda (n0: nat).(eq C c0 (CSort n0)))))) (let H8 \def (eq_ind_r T u2
 295 (\lambda (t: T).(getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) t)))
 296 H7 u1 H5) in (eq_ind T u1 (\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C
 297 (CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead
 298 e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c))))
 299 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda
 300 (n0: nat).(eq C (CSort x0) (CSort n0)))))) (let H9 \def (eq_ind K k (\lambda
 301 (k: K).(getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u1))) H8
 302 (Bind b) H4) in (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda (e:
 303 C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0
 304 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0
 305 (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1
 306 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0)))))) (eq_ind nat (r k0 n)
 307 (\lambda (n0: nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind
 308 b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b)
 309 u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 n0))) (\lambda (_:
 310 nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1:
 311 nat).(eq C (CSort x0) (CSort n1)))))) (eq_ind_r nat (S n) (\lambda (n0:
 312 nat).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e)))
 313 (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat
 314 (\lambda (_: nat).(eq nat (S n) n0)) (\lambda (_: nat).(eq K (Bind b) (Bind
 315 b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n1: nat).(eq C (CSort x0)
 316 (CSort n1)))))) (or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail
 317 (Bind b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b)
 318 u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (S n))) (\lambda (_: nat).(eq
 319 K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq
 320 C (CSort x0) (CSort n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat (S n) (S
 321 n))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1
 322 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0))) x0 (refl_equal nat (S
 323 n)) (refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s
 324 k0 (r k0 n)) (s_r k0 n)) (clen c) H3) k H4)) u2 H5)) c2 H6))))))) H2))
 325 H1))))])))))) c1)))))).
 326