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