matita/matita/contribs/lambdadelta/basic_1/wcpr0/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/wcpr0/defs.ma".
  18
  19 include "Basic-1/getl/props.ma".
  20
  21 theorem wcpr0_drop:
  22  \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
  23 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c1 (CHead
  24 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c2
  25 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda
  26 (_: C).(\lambda (u2: T).(pr0 u1 u2)))))))))))
  27 \def
  28  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c1 c2)).(wcpr0_ind
  29 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
  30 (u1: T).(\forall (k: K).((drop h O c (CHead e1 k u1)) \to (ex3_2 C T (\lambda
  31 (e2: C).(\lambda (u2: T).(drop h O c0 (CHead e2 k u2)))) (\lambda (e2:
  32 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
  33 u2))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
  34 (u1: T).(\lambda (k: K).(\lambda (H0: (drop h O c (CHead e1 k
  35 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead
  36 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
  37 C).(\lambda (u2: T).(pr0 u1 u2))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
  38 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
  39 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
  40 T).(\forall (k: K).((drop h O c3 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
  41 (e2: C).(\lambda (u2: T).(drop h O c4 (CHead e2 k u2)))) (\lambda (e2:
  42 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
  43 u2))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
  44 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
  45 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c3 k u1) (CHead
  46 e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead
  47 c4 k u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
  48 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) (\lambda (e1:
  49 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c3 k u1)
  50 (CHead e1 k0 u0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
  51 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c3 | (CHead c _ _)
  52 \Rightarrow c])) (CHead c3 k u1) (CHead e1 k0 u0) (drop_gen_refl (CHead c3 k
  53 u1) (CHead e1 k0 u0) H3)) in ((let H5 \def (f_equal C K (\lambda (e:
  54 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
  55 (CHead _ k1 _) \Rightarrow k1])) (CHead c3 k u1) (CHead e1 k0 u0)
  56 (drop_gen_refl (CHead c3 k u1) (CHead e1 k0 u0) H3)) in ((let H6 \def
  57 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
  58 [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c3 k u1)
  59 (CHead e1 k0 u0) (drop_gen_refl (CHead c3 k u1) (CHead e1 k0 u0) H3)) in
  60 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c3 e1)).(eq_ind K k (\lambda
  61 (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k
  62 u2) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
  63 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))))) (eq_ind T u1 (\lambda (t:
  64 T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k u2)
  65 (CHead e2 k u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda
  66 (_: C).(\lambda (u3: T).(pr0 t u3))))) (eq_ind C c3 (\lambda (c: C).(ex3_2 C
  67 T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k u2) (CHead e2 k
  68 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 c e2))) (\lambda (_:
  69 C).(\lambda (u3: T).(pr0 u1 u3))))) (ex3_2_intro C T (\lambda (e2:
  70 C).(\lambda (u3: T).(drop O O (CHead c4 k u2) (CHead e2 k u3)))) (\lambda
  71 (e2: C).(\lambda (_: T).(wcpr0 c3 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
  72 u1 u3))) c4 u2 (drop_refl (CHead c4 k u2)) H0 H2) e1 H8) u0 H6) k0 H7))))
  73 H5)) H4)))))) (K_ind (\lambda (k0: K).(\forall (n: nat).(((\forall (e1:
  74 C).(\forall (u3: T).(\forall (k1: K).((drop n O (CHead c3 k0 u1) (CHead e1 k1
  75 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 k0
  76 u2) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
  77 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) \to (\forall (e1:
  78 C).(\forall (u3: T).(\forall (k1: K).((drop (S n) O (CHead c3 k0 u1) (CHead
  79 e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop (S n) O
  80 (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
  81 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))))) (\lambda (b:
  82 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
  83 (k0: K).((drop n O (CHead c3 (Bind b) u1) (CHead e1 k0 u3)) \to (ex3_2 C T
  84 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 (Bind b) u2) (CHead e2
  85 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
  86 C).(\lambda (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0:
  87 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c3 (Bind b) u1) (CHead
  88 e1 k0 u0))).(let H5 \def (H1 n e1 u0 k0 (drop_gen_drop (Bind b) c3 (CHead e1
  89 k0 u0) u1 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop n
  90 O c4 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
  91 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) (ex3_2 C T (\lambda (e2:
  92 C).(\lambda (u3: T).(drop (S n) O (CHead c4 (Bind b) u2) (CHead e2 k0 u3))))
  93 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
  94 (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
  95 n O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0
  96 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O (CHead
  97 c4 (Bind b) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
  98 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1 (drop_drop
  99 (Bind b) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) (\lambda (f:
 100 F).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
 101 (k0: K).((drop n O (CHead c3 (Flat f) u1) (CHead e1 k0 u3)) \to (ex3_2 C T
 102 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 (Flat f) u2) (CHead e2
 103 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
 104 C).(\lambda (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0:
 105 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c3 (Flat f) u1) (CHead
 106 e1 k0 u0))).(let H5 \def (H1 (S n) e1 u0 k0 (drop_gen_drop (Flat f) c3 (CHead
 107 e1 k0 u0) u1 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop
 108 (S n) O c4 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
 109 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) (ex3_2 C T (\lambda (e2:
 110 C).(\lambda (u3: T).(drop (S n) O (CHead c4 (Flat f) u2) (CHead e2 k0 u3))))
 111 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
 112 (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
 113 (S n) O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0
 114 u0 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
 115 (CHead c4 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_:
 116 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1
 117 (drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k)
 118 h)))))))))) c1 c2 H))).
 119 (* COMMENTS
 120 Initial nodes: 1755
 121 END *)
 122
 123 theorem wcpr0_drop_back:
 124  \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
 125 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c1 (CHead
 126 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c2
 127 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda
 128 (_: C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
 129 \def
 130  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(wcpr0_ind
 131 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
 132 (u1: T).(\forall (k: K).((drop h O c0 (CHead e1 k u1)) \to (ex3_2 C T
 133 (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead e2 k u2)))) (\lambda
 134 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0
 135 u2 u1))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
 136 (u1: T).(\lambda (k: K).(\lambda (H0: (drop h O c (CHead e1 k
 137 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead
 138 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
 139 C).(\lambda (u2: T).(pr0 u2 u1))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
 140 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
 141 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
 142 T).(\forall (k: K).((drop h O c4 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
 143 (e2: C).(\lambda (u2: T).(drop h O c3 (CHead e2 k u2)))) (\lambda (e2:
 144 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
 145 u1))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
 146 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
 147 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c4 k u2) (CHead
 148 e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead
 149 c3 k u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 150 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) (\lambda (e1:
 151 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c4 k u2)
 152 (CHead e1 k0 u0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
 153 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c4 | (CHead c _ _)
 154 \Rightarrow c])) (CHead c4 k u2) (CHead e1 k0 u0) (drop_gen_refl (CHead c4 k
 155 u2) (CHead e1 k0 u0) H3)) in ((let H5 \def (f_equal C K (\lambda (e:
 156 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
 157 (CHead _ k1 _) \Rightarrow k1])) (CHead c4 k u2) (CHead e1 k0 u0)
 158 (drop_gen_refl (CHead c4 k u2) (CHead e1 k0 u0) H3)) in ((let H6 \def
 159 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 160 [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c4 k u2)
 161 (CHead e1 k0 u0) (drop_gen_refl (CHead c4 k u2) (CHead e1 k0 u0) H3)) in
 162 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c4 e1)).(eq_ind K k (\lambda
 163 (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k
 164 u1) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 165 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))))) (eq_ind T u2 (\lambda (t:
 166 T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k u1)
 167 (CHead e2 k u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda
 168 (_: C).(\lambda (u3: T).(pr0 u3 t))))) (eq_ind C c4 (\lambda (c: C).(ex3_2 C
 169 T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k u1) (CHead e2 k
 170 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 c))) (\lambda (_:
 171 C).(\lambda (u3: T).(pr0 u3 u2))))) (ex3_2_intro C T (\lambda (e2:
 172 C).(\lambda (u3: T).(drop O O (CHead c3 k u1) (CHead e2 k u3)))) (\lambda
 173 (e2: C).(\lambda (_: T).(wcpr0 e2 c4))) (\lambda (_: C).(\lambda (u3: T).(pr0
 174 u3 u2))) c3 u1 (drop_refl (CHead c3 k u1)) H0 H2) e1 H8) u0 H6) k0 H7))))
 175 H5)) H4)))))) (K_ind (\lambda (k0: K).(\forall (n: nat).(((\forall (e1:
 176 C).(\forall (u3: T).(\forall (k1: K).((drop n O (CHead c4 k0 u2) (CHead e1 k1
 177 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 k0
 178 u1) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 179 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) \to (\forall (e1:
 180 C).(\forall (u3: T).(\forall (k1: K).((drop (S n) O (CHead c4 k0 u2) (CHead
 181 e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop (S n) O
 182 (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
 183 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))))) (\lambda (b:
 184 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
 185 (k0: K).((drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)) \to (ex3_2 C T
 186 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 (Bind b) u1) (CHead e2
 187 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
 188 C).(\lambda (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0:
 189 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c4 (Bind b) u2) (CHead
 190 e1 k0 u0))).(let H5 \def (H1 n e1 u0 k0 (drop_gen_drop (Bind b) c4 (CHead e1
 191 k0 u0) u2 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop n
 192 O c3 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 193 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) (ex3_2 C T (\lambda (e2:
 194 C).(\lambda (u3: T).(drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3))))
 195 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
 196 (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
 197 n O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1
 198 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O (CHead
 199 c3 (Bind b) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
 200 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1 (drop_drop
 201 (Bind b) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) (\lambda (f:
 202 F).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
 203 (k0: K).((drop n O (CHead c4 (Flat f) u2) (CHead e1 k0 u3)) \to (ex3_2 C T
 204 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 (Flat f) u1) (CHead e2
 205 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
 206 C).(\lambda (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0:
 207 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c4 (Flat f) u2) (CHead
 208 e1 k0 u0))).(let H5 \def (H1 (S n) e1 u0 k0 (drop_gen_drop (Flat f) c4 (CHead
 209 e1 k0 u0) u2 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop
 210 (S n) O c3 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
 211 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) (ex3_2 C T (\lambda (e2:
 212 C).(\lambda (u3: T).(drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3))))
 213 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
 214 (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
 215 (S n) O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0
 216 x1 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
 217 (CHead c3 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_:
 218 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1
 219 (drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k)
 220 h)))))))))) c2 c1 H))).
 221 (* COMMENTS
 222 Initial nodes: 1755
 223 END *)
 224
 225 theorem wcpr0_getl:
 226  \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
 227 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
 228 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
 229 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
 230 C).(\lambda (u2: T).(pr0 u1 u2)))))))))))
 231 \def
 232  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c1 c2)).(wcpr0_ind
 233 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
 234 (u1: T).(\forall (k: K).((getl h c (CHead e1 k u1)) \to (ex3_2 C T (\lambda
 235 (e2: C).(\lambda (u2: T).(getl h c0 (CHead e2 k u2)))) (\lambda (e2:
 236 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
 237 u2))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
 238 (u1: T).(\lambda (k: K).(\lambda (H0: (getl h c (CHead e1 k
 239 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(getl h c (CHead e2
 240 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
 241 C).(\lambda (u2: T).(pr0 u1 u2))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
 242 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
 243 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
 244 T).(\forall (k: K).((getl h c3 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2:
 245 C).(\lambda (u2: T).(getl h c4 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda
 246 (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
 247 u2))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
 248 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
 249 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 k u1) (CHead e1
 250 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c4 k
 251 u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
 252 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) (\lambda (e1:
 253 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (getl O (CHead c3 k u1)
 254 (CHead e1 k0 u0))).(K_ind (\lambda (k1: K).((clear (CHead c3 k1 u1) (CHead e1
 255 k0 u0)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4 k1
 256 u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
 257 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))))) (\lambda (b: B).(\lambda
 258 (H4: (clear (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let H5 \def (f_equal C
 259 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 260 \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 k0 u0) (CHead c3
 261 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in ((let H6 \def
 262 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
 263 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead e1 k0 u0)
 264 (CHead c3 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in ((let
 265 H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
 266 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e1 k0
 267 u0) (CHead c3 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in
 268 (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1 c3)).(eq_ind_r K
 269 (Bind b) (\lambda (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl
 270 O (CHead c4 (Bind b) u2) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_:
 271 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))))) (eq_ind_r
 272 T u1 (\lambda (t: T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O
 273 (CHead c4 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda
 274 (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 t u3)))))
 275 (eq_ind_r C c3 (\lambda (c: C).(ex3_2 C T (\lambda (e2: C).(\lambda (u3:
 276 T).(getl O (CHead c4 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2:
 277 C).(\lambda (_: T).(wcpr0 c e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1
 278 u3))))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4
 279 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda (_:
 280 T).(wcpr0 c3 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) c4 u2
 281 (getl_refl b c4 u2) H0 H2) e1 H9) u0 H7) k0 H8)))) H6)) H5)))) (\lambda (f:
 282 F).(\lambda (H4: (clear (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let H5
 283 \def (H1 O e1 u0 k0 (getl_intro O c3 (CHead e1 k0 u0) c3 (drop_refl c3)
 284 (clear_gen_flat f c3 (CHead e1 k0 u0) u1 H4))) in (ex3_2_ind C T (\lambda
 285 (e2: C).(\lambda (u3: T).(getl O c4 (CHead e2 k0 u3)))) (\lambda (e2:
 286 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0
 287 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4 (Flat f)
 288 u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
 289 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda
 290 (x1: T).(\lambda (H6: (getl O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1
 291 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda
 292 (u3: T).(getl O (CHead c4 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2:
 293 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0
 294 u3))) x0 x1 (getl_flat c4 (CHead x0 k0 x1) O H6 f u2) H7 H8)))))) H5)))) k
 295 (getl_gen_O (CHead c3 k u1) (CHead e1 k0 u0) H3)))))) (K_ind (\lambda (k0:
 296 K).(\forall (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1:
 297 K).((getl n (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
 298 C).(\lambda (u4: T).(getl n (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda
 299 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0
 300 u3 u4))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((getl
 301 (S n) (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
 302 C).(\lambda (u4: T).(getl (S n) (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda
 303 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0
 304 u3 u4))))))))))) (\lambda (b: B).(\lambda (n: nat).(\lambda (_: ((\forall
 305 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 (Bind b) u1)
 306 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
 307 (CHead c4 (Bind b) u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
 308 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
 309 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
 310 (getl (S n) (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let H5 \def (H1 n e1
 311 u0 k0 (getl_gen_S (Bind b) c3 (CHead e1 k0 u0) u1 n H4)) in (ex3_2_ind C T
 312 (\lambda (e2: C).(\lambda (u3: T).(getl n c4 (CHead e2 k0 u3)))) (\lambda
 313 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
 314 u0 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c4
 315 (Bind b) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
 316 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0:
 317 C).(\lambda (x1: T).(\lambda (H6: (getl n c4 (CHead x0 k0 x1))).(\lambda (H7:
 318 (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2:
 319 C).(\lambda (u3: T).(getl (S n) (CHead c4 (Bind b) u2) (CHead e2 k0 u3))))
 320 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
 321 (u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Bind b) n c4 (CHead x0 k0 x1) H6 u2)
 322 H7 H8)))))) H5))))))))) (\lambda (f: F).(\lambda (n: nat).(\lambda (_:
 323 ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 (Flat
 324 f) u1) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4:
 325 T).(getl n (CHead c4 (Flat f) u2) (CHead e2 k0 u4)))) (\lambda (e2:
 326 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
 327 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
 328 (getl (S n) (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let H5 \def (H1 (S n)
 329 e1 u0 k0 (getl_gen_S (Flat f) c3 (CHead e1 k0 u0) u1 n H4)) in (ex3_2_ind C T
 330 (\lambda (e2: C).(\lambda (u3: T).(getl (S n) c4 (CHead e2 k0 u3)))) (\lambda
 331 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
 332 u0 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c4
 333 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
 334 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0:
 335 C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c4 (CHead x0 k0 x1))).(\lambda
 336 (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2:
 337 C).(\lambda (u3: T).(getl (S n) (CHead c4 (Flat f) u2) (CHead e2 k0 u3))))
 338 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
 339 (u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2)
 340 H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
 341 (* COMMENTS
 342 Initial nodes: 2103
 343 END *)
 344
 345 theorem wcpr0_getl_back:
 346  \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
 347 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
 348 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
 349 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
 350 C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
 351 \def
 352  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(wcpr0_ind
 353 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
 354 (u1: T).(\forall (k: K).((getl h c0 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
 355 (e2: C).(\lambda (u2: T).(getl h c (CHead e2 k u2)))) (\lambda (e2:
 356 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
 357 u1))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
 358 (u1: T).(\lambda (k: K).(\lambda (H0: (getl h c (CHead e1 k
 359 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(getl h c (CHead e2
 360 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
 361 C).(\lambda (u2: T).(pr0 u2 u1))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
 362 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
 363 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
 364 T).(\forall (k: K).((getl h c4 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2:
 365 C).(\lambda (u2: T).(getl h c3 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda
 366 (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
 367 u1))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
 368 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
 369 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 k u2) (CHead e1
 370 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c3 k
 371 u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 372 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) (\lambda (e1:
 373 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (getl O (CHead c4 k u2)
 374 (CHead e1 k0 u0))).(K_ind (\lambda (k1: K).((clear (CHead c4 k1 u2) (CHead e1
 375 k0 u0)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3 k1
 376 u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 377 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))))) (\lambda (b: B).(\lambda
 378 (H4: (clear (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let H5 \def (f_equal C
 379 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 380 \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 k0 u0) (CHead c4
 381 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in ((let H6 \def
 382 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
 383 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead e1 k0 u0)
 384 (CHead c4 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in ((let
 385 H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
 386 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e1 k0
 387 u0) (CHead c4 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in
 388 (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1 c4)).(eq_ind_r K
 389 (Bind b) (\lambda (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl
 390 O (CHead c3 (Bind b) u1) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_:
 391 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))))) (eq_ind_r
 392 T u2 (\lambda (t: T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O
 393 (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda
 394 (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 t)))))
 395 (eq_ind_r C c4 (\lambda (c: C).(ex3_2 C T (\lambda (e2: C).(\lambda (u3:
 396 T).(getl O (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2:
 397 C).(\lambda (_: T).(wcpr0 e2 c))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
 398 u2))))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3
 399 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda (_:
 400 T).(wcpr0 e2 c4))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u2))) c3 u1
 401 (getl_refl b c3 u1) H0 H2) e1 H9) u0 H7) k0 H8)))) H6)) H5)))) (\lambda (f:
 402 F).(\lambda (H4: (clear (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let H5
 403 \def (H1 O e1 u0 k0 (getl_intro O c4 (CHead e1 k0 u0) c4 (drop_refl c4)
 404 (clear_gen_flat f c4 (CHead e1 k0 u0) u2 H4))) in (ex3_2_ind C T (\lambda
 405 (e2: C).(\lambda (u3: T).(getl O c3 (CHead e2 k0 u3)))) (\lambda (e2:
 406 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
 407 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3 (Flat f)
 408 u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
 409 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda
 410 (x1: T).(\lambda (H6: (getl O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0
 411 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda
 412 (u3: T).(getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2:
 413 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
 414 u0))) x0 x1 (getl_flat c3 (CHead x0 k0 x1) O H6 f u1) H7 H8)))))) H5)))) k
 415 (getl_gen_O (CHead c4 k u2) (CHead e1 k0 u0) H3)))))) (K_ind (\lambda (k0:
 416 K).(\forall (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1:
 417 K).((getl n (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
 418 C).(\lambda (u4: T).(getl n (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda
 419 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0
 420 u4 u3))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((getl
 421 (S n) (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
 422 C).(\lambda (u4: T).(getl (S n) (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda
 423 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0
 424 u4 u3))))))))))) (\lambda (b: B).(\lambda (n: nat).(\lambda (_: ((\forall
 425 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 (Bind b) u2)
 426 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
 427 (CHead c3 (Bind b) u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
 428 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
 429 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
 430 (getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let H5 \def (H1 n e1
 431 u0 k0 (getl_gen_S (Bind b) c4 (CHead e1 k0 u0) u2 n H4)) in (ex3_2_ind C T
 432 (\lambda (e2: C).(\lambda (u3: T).(getl n c3 (CHead e2 k0 u3)))) (\lambda
 433 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0
 434 u3 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c3
 435 (Bind b) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
 436 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0:
 437 C).(\lambda (x1: T).(\lambda (H6: (getl n c3 (CHead x0 k0 x1))).(\lambda (H7:
 438 (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2:
 439 C).(\lambda (u3: T).(getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3))))
 440 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
 441 (u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Bind b) n c3 (CHead x0 k0 x1) H6 u1)
 442 H7 H8)))))) H5))))))))) (\lambda (f: F).(\lambda (n: nat).(\lambda (_:
 443 ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 (Flat
 444 f) u2) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4:
 445 T).(getl n (CHead c3 (Flat f) u1) (CHead e2 k0 u4)))) (\lambda (e2:
 446 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
 447 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
 448 (getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let H5 \def (H1 (S n)
 449 e1 u0 k0 (getl_gen_S (Flat f) c4 (CHead e1 k0 u0) u2 n H4)) in (ex3_2_ind C T
 450 (\lambda (e2: C).(\lambda (u3: T).(getl (S n) c3 (CHead e2 k0 u3)))) (\lambda
 451 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0
 452 u3 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c3
 453 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
 454 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0:
 455 C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c3 (CHead x0 k0 x1))).(\lambda
 456 (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2:
 457 C).(\lambda (u3: T).(getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3))))
 458 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
 459 (u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1)
 460 H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).
 461 (* COMMENTS
 462 Initial nodes: 2103
 463 END *)
 464