matita/matita/contribs/lambdadelta/basic_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 "basic_1/csubt/fwd.ma".
  18
  19 include "basic_1/drop/fwd.ma".
  20
  21 lemma 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 with [O \Rightarrow
  58 False | (S _) \Rightarrow True])) I O H3) in (False_ind (ex2 C (\lambda (d2:
  59 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
  60 (Flat f) u)))) H5))))) (drop_gen_sort n1 (S n0) O (CHead d1 (Flat f) u)
  61 H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0
  62 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0
  63 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
  64 (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f) u))))))))).(\lambda (k:
  65 K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (d1: C).(\forall (u0:
  66 T).((drop (S n0) O (CHead c0 k0 u) (CHead d1 (Flat f) u0)) \to (ex2 C
  67 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
  68 k0 u) (CHead d2 (Flat f) u0))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda
  69 (d1: C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u)
  70 (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
  71 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda (d2:
  72 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
  73 (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
  74 x)).(\lambda (H5: (drop n0 O c3 (CHead x (Flat f) u0))).(ex_intro2 C (\lambda
  75 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
  76 u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Bind b) n0 c3 (CHead x (Flat f)
  77 u0) H5 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Flat f)
  78 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 c0 u
 107 t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda
 108 (H5: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Flat f)
 109 u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0
 110 O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 111 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f)
 112 u0)))) (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda (H7: (drop n0 O
 113 c3 (CHead x (Flat f) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2))
 114 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f)
 115 u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Flat f) u0) H7 u))))) (H c0
 116 c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Flat f) u0) t n0
 117 H5)))))))))))))) c1 c2 H0)))))) n))).
 118
 119 lemma csubt_drop_abbr:
 120  \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
 121 c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind
 122 Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 123 n O c2 (CHead d2 (Bind Abbr) u)))))))))))
 124 \def
 125  \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
 126 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u:
 127 T).((drop n0 O c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
 128 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr)
 129 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
 130 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
 131 (Bind Abbr) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
 132 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H0)) in
 133 (let H2 \def (csubt_gen_abbr g d1 c2 u H1) in (ex2_ind C (\lambda (e2: C).(eq
 134 C c2 (CHead e2 (Bind Abbr) u))) (\lambda (e2: C).(csubt g d1 e2)) (ex2 C
 135 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2
 136 (Bind Abbr) u)))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x (Bind Abbr)
 137 u))).(\lambda (H4: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abbr) u)
 138 (\lambda (c: C).(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 139 C).(drop O O c (CHead d2 (Bind Abbr) u))))) (ex_intro2 C (\lambda (d2:
 140 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abbr) u) (CHead
 141 d2 (Bind Abbr) u))) x H4 (drop_refl (CHead x (Bind Abbr) u))) c2 H3))))
 142 H2))))))))) (\lambda (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2:
 143 C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1
 144 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 145 (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))))))))))).(\lambda
 146 (c1: C).(\lambda (c2: C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda
 147 (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (u: T).((drop (S n0) O c
 148 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 149 (\lambda (d2: C).(drop (S n0) O c0 (CHead d2 (Bind Abbr) u))))))))) (\lambda
 150 (n1: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n0) O
 151 (CSort n1) (CHead d1 (Bind Abbr) u))).(and3_ind (eq C (CHead d1 (Bind Abbr)
 152 u) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (ex2 C (\lambda (d2: C).(csubt
 153 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr)
 154 u)))) (\lambda (_: (eq C (CHead d1 (Bind Abbr) u) (CSort n1))).(\lambda (H3:
 155 (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n0)
 156 (\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow
 157 True])) I O H3) in (False_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 158 (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
 159 H5))))) (drop_gen_sort n1 (S n0) O (CHead d1 (Bind Abbr) u) H1)))))) (\lambda
 160 (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (H2:
 161 ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr)
 162 u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
 163 n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda (k: K).(K_ind (\lambda
 164 (k0: K).(\forall (u: T).(\forall (d1: C).(\forall (u0: T).((drop (S n0) O
 165 (CHead c0 k0 u) (CHead d1 (Bind Abbr) u0)) \to (ex2 C (\lambda (d2: C).(csubt
 166 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind
 167 Abbr) u0))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda
 168 (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind
 169 Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 170 C).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g
 171 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
 172 Abbr) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5:
 173 (drop n0 O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt
 174 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2
 175 (Bind Abbr) u0))) x H4 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u0) H5
 176 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Bind Abbr) u0)
 177 u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda (d1: C).(\lambda
 178 (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind
 179 Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 180 C).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2:
 181 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u)
 182 (CHead d2 (Bind Abbr) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
 183 x)).(\lambda (H5: (drop (S n0) O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C
 184 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 185 (Flat f) u) (CHead d2 (Bind Abbr) u0))) x H4 (drop_drop (Flat f) n0 c3 (CHead
 186 x (Bind Abbr) u0) H5 u))))) (H2 d1 u0 (drop_gen_drop (Flat f) c0 (CHead d1
 187 (Bind Abbr) u0) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
 188 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
 189 T).((drop (S n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
 190 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr)
 191 u))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
 192 T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S
 193 n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind Abbr) u))).(ex2_ind C
 194 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
 195 (Bind Abbr) u))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 196 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda
 197 (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x
 198 (Bind Abbr) u))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 199 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u))) x H5
 200 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u) H6 u2))))) (H c0 c3 H1 d1 u
 201 (drop_gen_drop (Bind Void) c0 (CHead d1 (Bind Abbr) u) u1 n0 H4))))))))))))))
 202 (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_:
 203 ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr)
 204 u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
 205 n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda (u: T).(\lambda (t:
 206 T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1:
 207 C).(\lambda (u0: T).(\lambda (H5: (drop (S n0) O (CHead c0 (Bind Abst) t)
 208 (CHead d1 (Bind Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
 209 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda
 210 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind
 211 Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (x: C).(\lambda (H6: (csubt g
 212 d1 x)).(\lambda (H7: (drop n0 O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C
 213 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 214 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))) x H6 (drop_drop (Bind Abbr) n0 c3
 215 (CHead x (Bind Abbr) u0) H7 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind
 216 Abst) c0 (CHead d1 (Bind Abbr) u0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
 217
 218 lemma 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)))) (ex4_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 (_: C).(\lambda (u: T).(ty3 g d1 u
 225 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u 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)))) (ex4_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 (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3
 234 g d2 u t)))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g
 235 c1 c2)).(\lambda (d1: C).(\lambda (t: T).(\lambda (H0: (drop O O c1 (CHead d1
 236 (Bind Abst) t))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
 237 (CHead d1 (Bind Abst) t) (drop_gen_refl c1 (CHead d1 (Bind Abst) t) H0)) in
 238 (let H2 \def (csubt_gen_abst g d1 c2 t H1) in (or_ind (ex2 C (\lambda (e2:
 239 C).(eq C c2 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt g d1 e2)))
 240 (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
 241 v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2))) (\lambda (_:
 242 C).(\lambda (v2: T).(ty3 g d1 v2 t))) (\lambda (e2: C).(\lambda (v2: T).(ty3
 243 g e2 v2 t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 244 C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 245 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O
 246 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
 247 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H3: (ex2 C
 248 (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt
 249 g d1 e2)))).(ex2_ind C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) t)))
 250 (\lambda (e2: C).(csubt g d1 e2)) (or (ex2 C (\lambda (d2: C).(csubt g d1
 251 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
 252 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 253 (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
 254 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 255 (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x (Bind Abst) t))).(\lambda
 256 (H5: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c: C).(or
 257 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead
 258 d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 259 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c (CHead d2 (Bind Abbr)
 260 u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
 261 C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_introl (ex2 C (\lambda (d2:
 262 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
 263 d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 264 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x (Bind Abst) t)
 265 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
 266 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2:
 267 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
 268 d2 (Bind Abst) t))) x H5 (drop_refl (CHead x (Bind Abst) t)))) c2 H4)))) H3))
 269 (\lambda (H3: (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2
 270 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2)))
 271 (\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t))) (\lambda (e2: C).(\lambda
 272 (v2: T).(ty3 g e2 v2 t))))).(ex4_2_ind C T (\lambda (e2: C).(\lambda (v2:
 273 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 274 T).(csubt g d1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t)))
 275 (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))) (or (ex2 C (\lambda (d2:
 276 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t))))
 277 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 278 C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
 279 C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 280 d2 u t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead
 281 x0 (Bind Abbr) x1))).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (ty3 g d1
 282 x1 t)).(\lambda (H7: (ty3 g x0 x1 t)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
 283 (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 284 C).(drop O O c (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 285 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O
 286 O c (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
 287 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_intror (ex2 C
 288 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x0 (Bind
 289 Abbr) x1) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
 290 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x0
 291 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
 292 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))
 293 (ex4_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 294 (d2: C).(\lambda (u: T).(drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
 295 Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
 296 C).(\lambda (u: T).(ty3 g d2 u t))) x0 x1 H5 (drop_refl (CHead x0 (Bind Abbr)
 297 x1)) H6 H7)) c2 H4))))))) H3)) H2))))))))) (\lambda (n0: nat).(\lambda (H:
 298 ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
 299 C).(\forall (t: T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C
 300 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2
 301 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 302 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr)
 303 u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
 304 C).(\lambda (u: T).(ty3 g d2 u t))))))))))))).(\lambda (c1: C).(\lambda (c2:
 305 C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0:
 306 C).(\forall (d1: C).(\forall (t: T).((drop (S n0) O c (CHead d1 (Bind Abst)
 307 t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 308 (S n0) O c0 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
 309 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O c0
 310 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
 311 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (n1:
 312 nat).(\lambda (d1: C).(\lambda (t: T).(\lambda (H1: (drop (S n0) O (CSort n1)
 313 (CHead d1 (Bind Abst) t))).(and3_ind (eq C (CHead d1 (Bind Abst) t) (CSort
 314 n1)) (eq nat (S n0) O) (eq nat O O) (or (ex2 C (\lambda (d2: C).(csubt g d1
 315 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t))))
 316 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 317 C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
 318 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
 319 (u: T).(ty3 g d2 u t))))) (\lambda (_: (eq C (CHead d1 (Bind Abst) t) (CSort
 320 n1))).(\lambda (H3: (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5
 321 \def (eq_ind nat (S n0) (\lambda (ee: nat).(match ee with [O \Rightarrow
 322 False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2 C (\lambda
 323 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
 324 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 325 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2
 326 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
 327 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) H5))))) (drop_gen_sort n1 (S n0) O
 328 (CHead d1 (Bind Abst) t) H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
 329 (H1: (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (t: T).((drop
 330 (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt
 331 g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))
 332 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 333 C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
 334 C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 335 d2 u t)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u:
 336 T).(\forall (d1: C).(\forall (t: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1
 337 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 338 (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T
 339 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 340 (u0: T).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abbr) u0)))) (\lambda
 341 (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0:
 342 T).(ty3 g d2 u0 t)))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda (d1:
 343 C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead
 344 d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 345 (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 346 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 347 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g
 348 d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (or (ex2 C
 349 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 350 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
 351 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
 352 (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
 353 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 354 t))))) (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 355 C).(drop n0 O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2:
 356 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))
 357 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
 358 (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 359 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 360 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
 361 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 362 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6:
 363 (drop n0 O c3 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2:
 364 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
 365 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
 366 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 367 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0:
 368 T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
 369 (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0)
 370 O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t))) x H5 (drop_drop (Bind b)
 371 n0 c3 (CHead x (Bind Abst) t) H6 u)))))) H4)) (\lambda (H4: (ex4_2 C T
 372 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 373 (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
 374 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 375 t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
 376 (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))))
 377 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
 378 (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 379 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst)
 380 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 381 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
 382 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
 383 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x0: C).(\lambda (x1:
 384 T).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (drop n0 O c3 (CHead x0 (Bind
 385 Abbr) x1))).(\lambda (H7: (ty3 g d1 x1 t)).(\lambda (H8: (ty3 g x0 x1
 386 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 387 C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C
 388 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 389 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
 390 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
 391 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex4_2_intro C T (\lambda (d2:
 392 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 393 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
 394 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 395 g d2 u0 t))) x0 x1 H5 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H6
 396 u) H7 H8)))))))) H4)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind b) c0 (CHead d1
 397 (Bind Abst) t) u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda (d1:
 398 C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead
 399 d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 400 (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda
 401 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
 402 T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
 403 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 404 t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
 405 n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda
 406 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
 407 T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda
 408 (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0:
 409 T).(ty3 g d2 u0 t))))) (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 410 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C
 411 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead
 412 d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
 413 (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t))))
 414 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 415 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
 416 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
 417 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt
 418 g d1 x)).(\lambda (H6: (drop (S n0) O c3 (CHead x (Bind Abst) t))).(or_introl
 419 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
 420 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 421 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 422 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
 423 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 424 g d2 u0 t)))) (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 425 C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t))) x H5
 426 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abst) t) H6 u)))))) H4)) (\lambda
 427 (H4: (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 428 (d2: C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0))))
 429 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
 430 (u0: T).(ty3 g d2 u0 t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_:
 431 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O c3
 432 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
 433 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda
 434 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f)
 435 u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
 436 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
 437 c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0:
 438 T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))
 439 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (csubt g d1 x0)).(\lambda
 440 (H6: (drop (S n0) O c3 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g d1 x1
 441 t)).(\lambda (H8: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt
 442 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2
 443 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 444 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u)
 445 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
 446 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex4_2_intro C T
 447 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 448 (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0))))
 449 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
 450 (u0: T).(ty3 g d2 u0 t))) x0 x1 H5 (drop_drop (Flat f) n0 c3 (CHead x0 (Bind
 451 Abbr) x1) H6 u) H7 H8)))))))) H4)) (H2 d1 t (drop_gen_drop (Flat f) c0 (CHead
 452 d1 (Bind Abst) t) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
 453 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t:
 454 T).((drop (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
 455 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst)
 456 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 457 (d2: C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))
 458 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
 459 (u: T).(ty3 g d2 u t)))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b
 460 Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (t:
 461 T).(\lambda (H4: (drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind
 462 Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 463 C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
 464 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
 465 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1
 466 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (or (ex2 C (\lambda
 467 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
 468 u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
 469 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
 470 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
 471 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 472 (\lambda (H5: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
 473 n0 O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1
 474 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t))) (or (ex2 C
 475 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 476 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
 477 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O
 478 (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda
 479 (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 480 (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda (H7: (drop n0 O c3
 481 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 482 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst)
 483 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 484 (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind
 485 Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
 486 C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csubt g
 487 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2
 488 (Bind Abst) t))) x H6 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abst) t) H7
 489 u2)))))) H5)) (\lambda (H5: (ex4_2 C T (\lambda (d2: C).(\lambda (_:
 490 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c3 (CHead d2
 491 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
 492 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex4_2_ind C T (\lambda (d2:
 493 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
 494 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1
 495 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) (or (ex2 C (\lambda
 496 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
 497 u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
 498 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
 499 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
 500 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 501 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (csubt g d1 x0)).(\lambda
 502 (H7: (drop n0 O c3 (CHead x0 (Bind Abbr) x1))).(\lambda (H8: (ty3 g d1 x1
 503 t)).(\lambda (H9: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt
 504 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2
 505 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
 506 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2)
 507 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
 508 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex4_2_intro C T (\lambda
 509 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
 510 T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda
 511 (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3
 512 g d2 u t))) x0 x1 H6 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H7
 513 u2) H8 H9)))))))) H5)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind Void) c0 (CHead
 514 d1 (Bind Abst) t) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3:
 515 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t:
 516 T).((drop (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
 517 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst)
 518 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
 519 (d2: C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))
 520 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
 521 (u: T).(ty3 g d2 u t)))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_:
 522 (ty3 g c0 u t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (t0:
 523 T).(\lambda (H5: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind
 524 Abst) t0))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 525 C).(drop n0 O c3 (CHead d2 (Bind Abst) t0)))) (ex4_2 C T (\lambda (d2:
 526 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 527 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g
 528 d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (or (ex2 C
 529 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
 530 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex4_2 C T (\lambda (d2:
 531 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 532 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
 533 C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 534 g d2 u0 t0))))) (\lambda (H6: (ex2 C (\lambda (d2: C).(csubt g d1 d2))
 535 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t0))))).(ex2_ind C
 536 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
 537 (Bind Abst) t0))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 538 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
 539 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 540 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
 541 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
 542 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))) (\lambda (x: C).(\lambda (H7:
 543 (csubt g d1 x)).(\lambda (H8: (drop n0 O c3 (CHead x (Bind Abst)
 544 t0))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 545 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
 546 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 547 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
 548 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
 549 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex_intro2 C (\lambda (d2:
 550 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
 551 (CHead d2 (Bind Abst) t0))) x H7 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind
 552 Abst) t0) H8 u)))))) H6)) (\lambda (H6: (ex4_2 C T (\lambda (d2: C).(\lambda
 553 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3
 554 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
 555 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))).(ex4_2_ind C T
 556 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 557 (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
 558 (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
 559 t0))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
 560 n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex4_2 C T
 561 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
 562 (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))))
 563 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda
 564 (u0: T).(ty3 g d2 u0 t0))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H7:
 565 (csubt g d1 x0)).(\lambda (H8: (drop n0 O c3 (CHead x0 (Bind Abbr)
 566 x1))).(\lambda (H9: (ty3 g d1 x1 t0)).(\lambda (H10: (ty3 g x0 x1
 567 t0)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
 568 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
 569 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
 570 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
 571 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
 572 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex4_2_intro C T (\lambda (d2:
 573 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
 574 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
 575 C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 576 g d2 u0 t0))) x0 x1 H7 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind Abbr) x1)
 577 H8 u) H9 H10)))))))) H6)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst) c0
 578 (CHead d1 (Bind Abst) t0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
 579