matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.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 "LambdaDelta-1/csubt/fwd.ma".
  18
  19 include "LambdaDelta-1/drop/fwd.ma".
  20
  21 theorem csubt_drop_flat:
  22  \forall (g: G).(\forall (f: F).(\forall (n: nat).(\forall (c1: C).(\forall
  23 (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1
  24 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
  25 (d2: C).(drop n O c2 (CHead d2 (Flat f) u))))))))))))
  26 \def
  27  \lambda (g: G).(\lambda (f: F).(\lambda (n: nat).(nat_ind (\lambda (n0:
  28 nat).(\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
  29 C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda
  30 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Flat f)
  31 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
  32 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
  33 (Flat f) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
  34 (CHead d1 (Flat f) u) (drop_gen_refl c1 (CHead d1 (Flat f) u) H0)) in (let
  35 H_x \def (csubt_gen_flat g d1 c2 u f H1) in (let H2 \def H_x in (ex2_ind C
  36 (\lambda (e2: C).(eq C c2 (CHead e2 (Flat f) u))) (\lambda (e2: C).(csubt g
  37 d1 e2)) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O
  38 c2 (CHead d2 (Flat f) u)))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x
  39 (Flat f) u))).(\lambda (H4: (csubt g d1 x)).(eq_ind_r C (CHead x (Flat f) u)
  40 (\lambda (c: C).(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
  41 C).(drop O O c (CHead d2 (Flat f) u))))) (ex_intro2 C (\lambda (d2: C).(csubt
  42 g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Flat f) u) (CHead d2 (Flat f)
  43 u))) x H4 (drop_refl (CHead x (Flat f) u))) c2 H3)))) H2)))))))))) (\lambda
  44 (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2)
  45 \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Flat f) u))
  46 \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2
  47 (CHead d2 (Flat f) u)))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda
  48 (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0: C).(\forall
  49 (d1: C).(\forall (u: T).((drop (S n0) O c (CHead d1 (Flat f) u)) \to (ex2 C
  50 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c0 (CHead
  51 d2 (Flat f) u))))))))) (\lambda (n1: nat).(\lambda (d1: C).(\lambda (u:
  52 T).(\lambda (H1: (drop (S n0) O (CSort n1) (CHead d1 (Flat f) u))).(and3_ind
  53 (eq C (CHead d1 (Flat f) u) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (ex2 C
  54 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1)
  55 (CHead d2 (Flat f) u)))) (\lambda (_: (eq C (CHead d1 (Flat f) u) (CSort
  56 n1))).(\lambda (H3: (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5
  57 \def (eq_ind nat (S n0) (\lambda (ee: nat).(match ee in nat return (\lambda
  58 (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3)
  59 in (False_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
  60 (S n0) O (CSort n1) (CHead d2 (Flat f) u)))) H5))))) (drop_gen_sort n1 (S n0)
  61 O (CHead d1 (Flat f) u) H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
  62 (H1: (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (u: T).((drop
  63 (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1
  64 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
  65 u))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall
  66 (d1: C).(\forall (u0: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1 (Flat f)
  67 u0)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
  68 n0) O (CHead c3 k0 u) (CHead d2 (Flat f) u0))))))))) (\lambda (b: B).(\lambda
  69 (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead
  70 c0 (Bind b) u) (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g
  71 d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0))) (ex2 C
  72 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
  73 (Bind b) u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g
  74 d1 x)).(\lambda (H5: (drop n0 O c3 (CHead x (Flat f) u0))).(ex_intro2 C
  75 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
  76 (Bind b) u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Bind b) n0 c3 (CHead x
  77 (Flat f) u0) H5 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind b) c0 (CHead d1
  78 (Flat f) u0) u n0 H3)))))))) (\lambda (f0: F).(\lambda (u: T).(\lambda (d1:
  79 C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f0) u)
  80 (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
  81 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda
  82 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f0)
  83 u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
  84 x)).(\lambda (H5: (drop (S n0) O c3 (CHead x (Flat f) u0))).(ex_intro2 C
  85 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
  86 (Flat f0) u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Flat f0) n0 c3 (CHead
  87 x (Flat f) u0) H5 u))))) (H2 d1 u0 (drop_gen_drop (Flat f0) c0 (CHead d1
  88 (Flat f) u0) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
  89 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
  90 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
  91 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
  92 u))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
  93 T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S
  94 n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u))).(ex2_ind C (\lambda
  95 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f)
  96 u))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
  97 (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)))) (\lambda (x: C).(\lambda (H5:
  98 (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Flat f) u))).(ex_intro2
  99 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 100 (Bind b) u2) (CHead d2 (Flat f) u))) x H5 (drop_drop (Bind b) n0 c3 (CHead x
 101 (Flat f) u) H6 u2))))) (H c0 c3 H1 d1 u (drop_gen_drop (Bind Void) c0 (CHead
 102 d1 (Flat f) u) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3:
 103 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
 104 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
 105 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
 106 u))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c3 u
 107 t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H4: (drop (S n0) O (CHead c0
 108 (Bind Abst) t) (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g
 109 d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0))) (ex2 C
 110 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 111 (Bind Abbr) u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H5: (csubt
 112 g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Flat f) u0))).(ex_intro2 C
 113 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 114 (Bind Abbr) u) (CHead d2 (Flat f) u0))) x H5 (drop_drop (Bind Abbr) n0 c3
 115 (CHead x (Flat f) u0) H6 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind Abst)
 116 c0 (CHead d1 (Flat f) u0) t n0 H4))))))))))))) c1 c2 H0)))))) n))).
 117
 118 theorem csubt_drop_abbr:
 119  \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
 120 c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind
 121 Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 122 n O c2 (CHead d2 (Bind Abbr) u)))))))))))
 123 \def
 124  \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
 125 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u:
 126 T).((drop n0 O c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
 127 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr)
 128 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
 129 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
 130 (Bind Abbr) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
 131 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H0)) in
 132 (let H2 \def (csubt_gen_abbr g d1 c2 u H1) in (ex2_ind C (\lambda (e2: C).(eq
 133 C c2 (CHead e2 (Bind Abbr) u))) (\lambda (e2: C).(csubt g d1 e2)) (ex2 C
 134 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2
 135 (Bind Abbr) u)))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x (Bind Abbr)
 136 u))).(\lambda (H4: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abbr) u)
 137 (\lambda (c: C).(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 138 C).(drop O O c (CHead d2 (Bind Abbr) u))))) (ex_intro2 C (\lambda (d2:
 139 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abbr) u) (CHead
 140 d2 (Bind Abbr) u))) x H4 (drop_refl (CHead x (Bind Abbr) u))) c2 H3))))
 141 H2))))))))) (\lambda (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2:
 142 C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1
 143 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 144 (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))))))))))).(\lambda
 145 (c1: C).(\lambda (c2: C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda
 146 (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (u: T).((drop (S n0) O c
 147 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 148 (\lambda (d2: C).(drop (S n0) O c0 (CHead d2 (Bind Abbr) u))))))))) (\lambda
 149 (n1: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n0) O
 150 (CSort n1) (CHead d1 (Bind Abbr) u))).(and3_ind (eq C (CHead d1 (Bind Abbr)
 151 u) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (ex2 C (\lambda (d2: C).(csubt
 152 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr)
 153 u)))) (\lambda (_: (eq C (CHead d1 (Bind Abbr) u) (CSort n1))).(\lambda (H3:
 154 (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n0)
 155 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
 156 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (ex2 C
 157 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1)
 158 (CHead d2 (Bind Abbr) u)))) H5))))) (drop_gen_sort n1 (S n0) O (CHead d1
 159 (Bind Abbr) u) H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1:
 160 (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (u: T).((drop (S
 161 n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1
 162 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr)
 163 u))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall
 164 (d1: C).(\forall (u0: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1 (Bind
 165 Abbr) u0)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 166 C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abbr) u0))))))))) (\lambda
 167 (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H3: (drop
 168 (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abbr) u0))).(ex2_ind C
 169 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
 170 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 171 C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda
 172 (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5: (drop n0 O c3 (CHead x
 173 (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 174 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0))) x H4
 175 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u0) H5 u))))) (H c0 c3 H1 d1
 176 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Bind Abbr) u0) u n0 H3))))))))
 177 (\lambda (f: F).(\lambda (u: T).(\lambda (d1: C).(\lambda (u0: T).(\lambda
 178 (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abbr)
 179 u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
 180 n0) O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 181 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr)
 182 u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5: (drop (S
 183 n0) O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1
 184 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 185 Abbr) u0))) x H4 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abbr) u0) H5 u)))))
 186 (H2 d1 u0 (drop_gen_drop (Flat f) c0 (CHead d1 (Bind Abbr) u0) u n0
 187 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g
 188 c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0
 189 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 190 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda
 191 (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2:
 192 T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S n0) O (CHead c0
 193 (Bind Void) u1) (CHead d1 (Bind Abbr) u))).(ex2_ind C (\lambda (d2: C).(csubt
 194 g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr) u))) (ex2 C
 195 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 196 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (x: C).(\lambda (H5: (csubt
 197 g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Bind Abbr) u))).(ex_intro2 C
 198 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 199 (Bind b) u2) (CHead d2 (Bind Abbr) u))) x H5 (drop_drop (Bind b) n0 c3 (CHead
 200 x (Bind Abbr) u) H6 u2))))) (H c0 c3 H1 d1 u (drop_gen_drop (Bind Void) c0
 201 (CHead d1 (Bind Abbr) u) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda
 202 (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1:
 203 C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C
 204 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead
 205 d2 (Bind Abbr) u))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g
 206 c3 u t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda (H4: (drop (S n0) O
 207 (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abbr) u0))).(ex2_ind C (\lambda (d2:
 208 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr)
 209 u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0)
 210 O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (x:
 211 C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Bind
 212 Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 213 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))) x H5
 214 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind Abbr) u0) H6 u))))) (H c0 c3 H1
 215 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Bind Abbr) u0) t n0
 216 H4))))))))))))) c1 c2 H0)))))) n)).
 217
 218 theorem csubt_drop_abst:
 219  \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
 220 c1 c2) \to (\forall (d1: C).(\forall (t: T).((drop n O c1 (CHead d1 (Bind
 221 Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 222 C).(drop n O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 223 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n
 224 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 225 t))))))))))))
 226 \def
 227  \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
 228 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (t:
 229 T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
 230 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abst)
 231 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 232 (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda
 233 (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))))) (\lambda (c1: C).(\lambda
 234 (c2: C).(\lambda (H: (csubt g c1 c2)).(\lambda (d1: C).(\lambda (t:
 235 T).(\lambda (H0: (drop O O c1 (CHead d1 (Bind Abst) t))).(let H1 \def (eq_ind
 236 C c1 (\lambda (c: C).(csubt g c c2)) H (CHead d1 (Bind Abst) t)
 237 (drop_gen_refl c1 (CHead d1 (Bind Abst) t) H0)) in (let H2 \def
 238 (csubt_gen_abst g d1 c2 t H1) in (or_ind (ex2 C (\lambda (e2: C).(eq C c2
 239 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt g d1 e2))) (ex3_2 C T
 240 (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2))))
 241 (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2))) (\lambda (e2: C).(\lambda
 242 (v2: T).(ty3 g e2 v2 t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 243 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
 244 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
 245 T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 246 T).(ty3 g d2 u t))))) (\lambda (H3: (ex2 C (\lambda (e2: C).(eq C c2 (CHead
 247 e2 (Bind Abst) t))) (\lambda (e2: C).(csubt g d1 e2)))).(ex2_ind C (\lambda
 248 (e2: C).(eq C c2 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt g d1 e2))
 249 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2
 250 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 251 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c2 (CHead d2
 252 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 253 (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x (Bind Abst) t))).(\lambda
 254 (H5: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c: C).(or
 255 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead
 256 d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 257 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c (CHead d2 (Bind Abbr)
 258 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_introl (ex2 C
 259 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind
 260 Abst) t) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 261 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x
 262 (Bind Abst) t) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 263 T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 264 (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) t))) x H5
 265 (drop_refl (CHead x (Bind Abst) t)))) c2 H4)))) H3)) (\lambda (H3: (ex3_2 C T
 266 (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2))))
 267 (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2))) (\lambda (e2: C).(\lambda
 268 (v2: T).(ty3 g e2 v2 t))))).(ex3_2_ind C T (\lambda (e2: C).(\lambda (v2:
 269 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 270 T).(csubt g d1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))) (or
 271 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead
 272 d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 273 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr)
 274 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x0:
 275 C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead x0 (Bind Abbr)
 276 x1))).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (ty3 g x0 x1 t)).(eq_ind_r
 277 C (CHead x0 (Bind Abbr) x1) (\lambda (c: C).(or (ex2 C (\lambda (d2:
 278 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abst) t))))
 279 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 280 C).(\lambda (u: T).(drop O O c (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
 281 C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_intror (ex2 C (\lambda (d2:
 282 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x0 (Bind Abbr) x1)
 283 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 284 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x0
 285 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 286 T).(ty3 g d2 u t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt
 287 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x0 (Bind Abbr)
 288 x1) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 289 t))) x0 x1 H5 (drop_refl (CHead x0 (Bind Abbr) x1)) H6)) c2 H4)))))) H3))
 290 H2))))))))) (\lambda (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2:
 291 C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (t: T).((drop n0 O c1
 292 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 293 (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 294 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 295 (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda
 296 (u: T).(ty3 g d2 u t))))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda
 297 (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0: C).(\forall
 298 (d1: C).(\forall (t: T).((drop (S n0) O c (CHead d1 (Bind Abst) t)) \to (or
 299 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c0
 300 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 301 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O c0
 302 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 303 t)))))))))) (\lambda (n1: nat).(\lambda (d1: C).(\lambda (t: T).(\lambda (H1:
 304 (drop (S n0) O (CSort n1) (CHead d1 (Bind Abst) t))).(and3_ind (eq C (CHead
 305 d1 (Bind Abst) t) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (or (ex2 C
 306 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1)
 307 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 308 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CSort
 309 n1) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 310 t))))) (\lambda (_: (eq C (CHead d1 (Bind Abst) t) (CSort n1))).(\lambda (H3:
 311 (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n0)
 312 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
 313 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2
 314 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort
 315 n1) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 316 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CSort
 317 n1) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 318 t))))) H5))))) (drop_gen_sort n1 (S n0) O (CHead d1 (Bind Abst) t) H1))))))
 319 (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda
 320 (H2: ((\forall (d1: C).(\forall (t: T).((drop (S n0) O c0 (CHead d1 (Bind
 321 Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 322 C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 323 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
 324 (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3
 325 g d2 u t)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u:
 326 T).(\forall (d1: C).(\forall (t: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1
 327 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 328 (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 329 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 330 (u0: T).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abbr) u0)))) (\lambda
 331 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))))))) (\lambda (b: B).(\lambda
 332 (u: T).(\lambda (d1: C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead
 333 c0 (Bind b) u) (CHead d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2:
 334 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst)
 335 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 336 (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda
 337 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (or (ex2 C (\lambda (d2:
 338 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
 339 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 340 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 341 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 342 T).(ty3 g d2 u0 t))))) (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 343 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C
 344 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
 345 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 346 C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C
 347 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 348 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
 349 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda
 350 (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x
 351 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 352 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t))))
 353 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 354 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
 355 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex_intro2
 356 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 357 (Bind b) u) (CHead d2 (Bind Abst) t))) x H5 (drop_drop (Bind b) n0 c3 (CHead
 358 x (Bind Abst) t) H6 u)))))) H4)) (\lambda (H4: (ex3_2 C T (\lambda (d2:
 359 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 360 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g
 361 d2 u0 t))))).(ex3_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 362 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr)
 363 u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C
 364 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 365 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda
 366 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
 367 (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda
 368 (u0: T).(ty3 g d2 u0 t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5:
 369 (csubt g d1 x0)).(\lambda (H6: (drop n0 O c3 (CHead x0 (Bind Abbr)
 370 x1))).(\lambda (H7: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2:
 371 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
 372 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 373 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 374 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 375 T).(ty3 g d2 u0 t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_:
 376 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 377 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 378 T).(ty3 g d2 u0 t))) x0 x1 H5 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr)
 379 x1) H6 u) H7))))))) H4)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind b) c0 (CHead
 380 d1 (Bind Abst) t) u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda
 381 (d1: C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u)
 382 (CHead d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 383 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 384 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 385 (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
 386 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (or (ex2 C (\lambda (d2: C).(csubt g
 387 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 388 Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
 389 (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead
 390 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))
 391 (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 392 (S n0) O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g
 393 d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))) (or
 394 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
 395 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 396 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 397 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
 398 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt
 399 g d1 x)).(\lambda (H6: (drop (S n0) O c3 (CHead x (Bind Abst) t))).(or_introl
 400 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
 401 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 402 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 403 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
 404 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex_intro2 C (\lambda (d2: C).(csubt g
 405 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 406 Abst) t))) x H5 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abst) t) H6 u))))))
 407 H4)) (\lambda (H4: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 408 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind
 409 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))).(ex3_2_ind
 410 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 411 C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda
 412 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda (d2: C).(csubt
 413 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2
 414 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 415 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u)
 416 (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 417 t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (csubt g d1
 418 x0)).(\lambda (H6: (drop (S n0) O c3 (CHead x0 (Bind Abbr) x1))).(\lambda
 419 (H7: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 420 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst)
 421 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 422 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 423 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
 424 (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 425 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 426 Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) x0 x1 H5
 427 (drop_drop (Flat f) n0 c3 (CHead x0 (Bind Abbr) x1) H6 u) H7))))))) H4)) (H2
 428 d1 t (drop_gen_drop (Flat f) c0 (CHead d1 (Bind Abst) t) u n0 H3))))))))
 429 k)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0
 430 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t: T).((drop (S n0) O c0 (CHead
 431 d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 432 (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
 433 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
 434 T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda
 435 (u: T).(ty3 g d2 u t)))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b
 436 Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (t:
 437 T).(\lambda (H4: (drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind
 438 Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 439 C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 440 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
 441 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 442 d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 443 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C
 444 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 445 C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind
 446 Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H5:
 447 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3
 448 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
 449 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda
 450 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
 451 u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 452 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
 453 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 454 T).(ty3 g d2 u t))))) (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda
 455 (H7: (drop n0 O c3 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2:
 456 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2)
 457 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 458 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
 459 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 460 T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 461 (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t))) x H6
 462 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abst) t) H7 u2)))))) H5)) (\lambda
 463 (H5: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 464 (d2: C).(\lambda (u: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda
 465 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex3_2_ind C T (\lambda (d2:
 466 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
 467 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 468 d2 u t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 469 (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 470 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 471 (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u))))
 472 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x0: C).(\lambda
 473 (x1: T).(\lambda (H6: (csubt g d1 x0)).(\lambda (H7: (drop n0 O c3 (CHead x0
 474 (Bind Abbr) x1))).(\lambda (H8: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda
 475 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
 476 u2) (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 477 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
 478 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 479 T).(ty3 g d2 u t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt
 480 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b)
 481 u2) (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 482 t))) x0 x1 H6 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H7 u2)
 483 H8))))))) H5)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind Void) c0 (CHead d1 (Bind
 484 Abst) t) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
 485 (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t: T).((drop
 486 (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt
 487 g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))
 488 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 489 C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda
 490 (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))).(\lambda (u: T).(\lambda (t:
 491 T).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (t0: T).(\lambda
 492 (H4: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abst)
 493 t0))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 494 n0 O c3 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 495 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead
 496 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))
 497 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
 498 (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda
 499 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
 500 T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))))
 501 (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))) (\lambda (H5: (ex2 C
 502 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
 503 (Bind Abst) t0))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 504 (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t0))) (or (ex2 C (\lambda (d2:
 505 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
 506 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 507 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 508 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 509 T).(ty3 g d2 u0 t0))))) (\lambda (x: C).(\lambda (H6: (csubt g d1
 510 x)).(\lambda (H7: (drop n0 O c3 (CHead x (Bind Abst) t0))).(or_introl (ex2 C
 511 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 512 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2:
 513 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 514 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2:
 515 C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex_intro2 C (\lambda (d2: C).(csubt
 516 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2
 517 (Bind Abst) t0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind Abst) t0)
 518 H7 u)))))) H5)) (\lambda (H5: (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 519 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead
 520 d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 521 t0))))).(ex3_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
 522 (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))))
 523 (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))) (or (ex2 C (\lambda (d2:
 524 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
 525 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 526 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 527 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 528 T).(ty3 g d2 u0 t0))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6:
 529 (csubt g d1 x0)).(\lambda (H7: (drop n0 O c3 (CHead x0 (Bind Abbr)
 530 x1))).(\lambda (H8: (ty3 g x0 x1 t0)).(or_intror (ex2 C (\lambda (d2:
 531 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
 532 (CHead d2 (Bind Abst) t0)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 533 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 534 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 535 T).(ty3 g d2 u0 t0)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_:
 536 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 537 c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (d2: C).(\lambda (u0:
 538 T).(ty3 g d2 u0 t0))) x0 x1 H6 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind
 539 Abbr) x1) H7 u) H8))))))) H5)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst)
 540 c0 (CHead d1 (Bind Abst) t0) t n0 H4))))))))))))) c1 c2 H0)))))) n)).
 541