matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/getl.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/getl".
  18
  19 include "csub3/fwd.ma".
  20
  21 include "csub3/clear.ma".
  22
  23 include "csub3/drop.ma".
  24
  25 include "getl/clear.ma".
  26
  27 theorem csub3_getl_abbr:
  28  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
  29 (n: nat).((getl n c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csub3 g
  30 c1 c2) \to (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n
  31 c2 (CHead d2 (Bind Abbr) u)))))))))))
  32 \def
  33  \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda
  34 (n: nat).(\lambda (H: (getl n c1 (CHead d1 (Bind Abbr) u))).(let H0 \def
  35 (getl_gen_all c1 (CHead d1 (Bind Abbr) u) n H) in (ex2_ind C (\lambda (e:
  36 C).(drop n O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abbr) u)))
  37 (\forall (c2: C).((csub3 g c1 c2) \to (ex2 C (\lambda (d2: C).(csub3 g d1
  38 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u)))))) (\lambda (x:
  39 C).(\lambda (H1: (drop n O c1 x)).(\lambda (H2: (clear x (CHead d1 (Bind
  40 Abbr) u))).((match x in C return (\lambda (c: C).((drop n O c1 c) \to ((clear
  41 c (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csub3 g c1 c2) \to (ex2 C
  42 (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind
  43 Abbr) u))))))))) with [(CSort n0) \Rightarrow (\lambda (_: (drop n O c1
  44 (CSort n0))).(\lambda (H4: (clear (CSort n0) (CHead d1 (Bind Abbr)
  45 u))).(clear_gen_sort (CHead d1 (Bind Abbr) u) n0 H4 (\forall (c2: C).((csub3
  46 g c1 c2) \to (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl
  47 n c2 (CHead d2 (Bind Abbr) u))))))))) | (CHead c k t) \Rightarrow (\lambda
  48 (H3: (drop n O c1 (CHead c k t))).(\lambda (H4: (clear (CHead c k t) (CHead
  49 d1 (Bind Abbr) u))).((match k in K return (\lambda (k0: K).((drop n O c1
  50 (CHead c k0 t)) \to ((clear (CHead c k0 t) (CHead d1 (Bind Abbr) u)) \to
  51 (\forall (c2: C).((csub3 g c1 c2) \to (ex2 C (\lambda (d2: C).(csub3 g d1
  52 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))))))))) with [(Bind
  53 b) \Rightarrow (\lambda (H5: (drop n O c1 (CHead c (Bind b) t))).(\lambda
  54 (H6: (clear (CHead c (Bind b) t) (CHead d1 (Bind Abbr) u))).(let H7 \def
  55 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
  56 [(CSort _) \Rightarrow d1 | (CHead c0 _ _) \Rightarrow c0])) (CHead d1 (Bind
  57 Abbr) u) (CHead c (Bind b) t) (clear_gen_bind b c (CHead d1 (Bind Abbr) u) t
  58 H6)) in ((let H8 \def (f_equal C B (\lambda (e: C).(match e in C return
  59 (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _)
  60 \Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b0)
  61 \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u)
  62 (CHead c (Bind b) t) (clear_gen_bind b c (CHead d1 (Bind Abbr) u) t H6)) in
  63 ((let H9 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
  64 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
  65 d1 (Bind Abbr) u) (CHead c (Bind b) t) (clear_gen_bind b c (CHead d1 (Bind
  66 Abbr) u) t H6)) in (\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1
  67 c)).(\lambda (c2: C).(\lambda (H12: (csub3 g c1 c2)).(let H13 \def (eq_ind_r
  68 T t (\lambda (t0: T).(drop n O c1 (CHead c (Bind b) t0))) H5 u H9) in (let
  69 H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead c (Bind b0) u)))
  70 H13 Abbr H10) in (let H15 \def (eq_ind_r C c (\lambda (c0: C).(drop n O c1
  71 (CHead c0 (Bind Abbr) u))) H14 d1 H11) in (ex2_ind C (\lambda (d2: C).(csub3
  72 g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abbr) u))) (ex2 C
  73 (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind
  74 Abbr) u)))) (\lambda (x0: C).(\lambda (H16: (csub3 g d1 x0)).(\lambda (H17:
  75 (drop n O c2 (CHead x0 (Bind Abbr) u))).(ex_intro2 C (\lambda (d2: C).(csub3
  76 g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))) x0 H16
  77 (getl_intro n c2 (CHead x0 (Bind Abbr) u) (CHead x0 (Bind Abbr) u) H17
  78 (clear_bind Abbr x0 u)))))) (csub3_drop_abbr g n c1 c2 H12 d1 u H15))))))))))
  79 H8)) H7)))) | (Flat f) \Rightarrow (\lambda (H5: (drop n O c1 (CHead c (Flat
  80 f) t))).(\lambda (H6: (clear (CHead c (Flat f) t) (CHead d1 (Bind Abbr)
  81 u))).(let H7 \def H5 in (unintro C c1 (\lambda (c0: C).((drop n O c0 (CHead c
  82 (Flat f) t)) \to (\forall (c2: C).((csub3 g c0 c2) \to (ex2 C (\lambda (d2:
  83 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr)
  84 u)))))))) (nat_ind (\lambda (n0: nat).(\forall (x0: C).((drop n0 O x0 (CHead
  85 c (Flat f) t)) \to (\forall (c2: C).((csub3 g x0 c2) \to (ex2 C (\lambda (d2:
  86 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n0 c2 (CHead d2 (Bind Abbr)
  87 u))))))))) (\lambda (x0: C).(\lambda (H8: (drop O O x0 (CHead c (Flat f)
  88 t))).(\lambda (c2: C).(\lambda (H9: (csub3 g x0 c2)).(let H10 \def (eq_ind C
  89 x0 (\lambda (c0: C).(csub3 g c0 c2)) H9 (CHead c (Flat f) t) (drop_gen_refl
  90 x0 (CHead c (Flat f) t) H8)) in (let H_y \def (clear_flat c (CHead d1 (Bind
  91 Abbr) u) (clear_gen_flat f c (CHead d1 (Bind Abbr) u) t H6) f t) in (let H11
  92 \def (csub3_clear_conf g (CHead c (Flat f) t) c2 H10 (CHead d1 (Bind Abbr) u)
  93 H_y) in (ex2_ind C (\lambda (e2: C).(csub3 g (CHead d1 (Bind Abbr) u) e2))
  94 (\lambda (e2: C).(clear c2 e2)) (ex2 C (\lambda (d2: C).(csub3 g d1 d2))
  95 (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (x1:
  96 C).(\lambda (H12: (csub3 g (CHead d1 (Bind Abbr) u) x1)).(\lambda (H13:
  97 (clear c2 x1)).(let H14 \def (csub3_gen_abbr g d1 x1 u H12) in (ex2_ind C
  98 (\lambda (e2: C).(eq C x1 (CHead e2 (Bind Abbr) u))) (\lambda (e2: C).(csub3
  99 g d1 e2)) (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl O
 100 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (x2: C).(\lambda (H15: (eq C x1
 101 (CHead x2 (Bind Abbr) u))).(\lambda (H16: (csub3 g d1 x2)).(let H17 \def
 102 (eq_ind C x1 (\lambda (c0: C).(clear c2 c0)) H13 (CHead x2 (Bind Abbr) u)
 103 H15) in (ex_intro2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl
 104 O c2 (CHead d2 (Bind Abbr) u))) x2 H16 (getl_intro O c2 (CHead x2 (Bind Abbr)
 105 u) c2 (drop_refl c2) H17)))))) H14))))) H11)))))))) (\lambda (n0:
 106 nat).(\lambda (H8: ((\forall (x0: C).((drop n0 O x0 (CHead c (Flat f) t)) \to
 107 (\forall (c2: C).((csub3 g x0 c2) \to (ex2 C (\lambda (d2: C).(csub3 g d1
 108 d2)) (\lambda (d2: C).(getl n0 c2 (CHead d2 (Bind Abbr) u)))))))))).(\lambda
 109 (x0: C).(\lambda (H9: (drop (S n0) O x0 (CHead c (Flat f) t))).(\lambda (c2:
 110 C).(\lambda (H10: (csub3 g x0 c2)).(let H11 \def (drop_clear x0 (CHead c
 111 (Flat f) t) n0 H9) in (ex2_3_ind B C T (\lambda (b: B).(\lambda (e:
 112 C).(\lambda (v: T).(clear x0 (CHead e (Bind b) v))))) (\lambda (_:
 113 B).(\lambda (e: C).(\lambda (_: T).(drop n0 O e (CHead c (Flat f) t))))) (ex2
 114 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead
 115 d2 (Bind Abbr) u)))) (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3:
 116 T).(\lambda (H12: (clear x0 (CHead x2 (Bind x1) x3))).(\lambda (H13: (drop n0
 117 O x2 (CHead c (Flat f) t))).(let H14 \def (csub3_clear_conf g x0 c2 H10
 118 (CHead x2 (Bind x1) x3) H12) in (ex2_ind C (\lambda (e2: C).(csub3 g (CHead
 119 x2 (Bind x1) x3) e2)) (\lambda (e2: C).(clear c2 e2)) (ex2 C (\lambda (d2:
 120 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr)
 121 u)))) (\lambda (x4: C).(\lambda (H15: (csub3 g (CHead x2 (Bind x1) x3)
 122 x4)).(\lambda (H16: (clear c2 x4)).(let H17 \def (csub3_gen_bind g x1 x2 x4
 123 x3 H15) in (ex2_3_ind B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 124 T).(eq C x4 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 125 C).(\lambda (_: T).(csub3 g x2 e2)))) (ex2 C (\lambda (d2: C).(csub3 g d1
 126 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda
 127 (x5: B).(\lambda (x6: C).(\lambda (x7: T).(\lambda (H18: (eq C x4 (CHead x6
 128 (Bind x5) x7))).(\lambda (H19: (csub3 g x2 x6)).(let H20 \def (eq_ind C x4
 129 (\lambda (c0: C).(clear c2 c0)) H16 (CHead x6 (Bind x5) x7) H18) in (let H21
 130 \def (H8 x2 H13 x6 H19) in (ex2_ind C (\lambda (d2: C).(csub3 g d1 d2))
 131 (\lambda (d2: C).(getl n0 x6 (CHead d2 (Bind Abbr) u))) (ex2 C (\lambda (d2:
 132 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr)
 133 u)))) (\lambda (x8: C).(\lambda (H22: (csub3 g d1 x8)).(\lambda (H23: (getl
 134 n0 x6 (CHead x8 (Bind Abbr) u))).(ex_intro2 C (\lambda (d2: C).(csub3 g d1
 135 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr) u))) x8 H22
 136 (getl_clear_bind x5 c2 x6 x7 H20 (CHead x8 (Bind Abbr) u) n0 H23)))))
 137 H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))]) H3 H4)))]) H1 H2))))
 138 H0))))))).
 139
 140 theorem csub3_getl_abst:
 141  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (t: T).(\forall
 142 (n: nat).((getl n c1 (CHead d1 (Bind Abst) t)) \to (\forall (c2: C).((csub3 g
 143 c1 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 144 C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 145 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 146 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 147 t))))))))))))
 148 \def
 149  \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (t: T).(\lambda
 150 (n: nat).(\lambda (H: (getl n c1 (CHead d1 (Bind Abst) t))).(let H0 \def
 151 (getl_gen_all c1 (CHead d1 (Bind Abst) t) n H) in (ex2_ind C (\lambda (e:
 152 C).(drop n O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abst) t)))
 153 (\forall (c2: C).((csub3 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1
 154 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 155 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 156 (u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 157 T).(ty3 g d2 u t))))))) (\lambda (x: C).(\lambda (H1: (drop n O c1
 158 x)).(\lambda (H2: (clear x (CHead d1 (Bind Abst) t))).((match x in C return
 159 (\lambda (c: C).((drop n O c1 c) \to ((clear c (CHead d1 (Bind Abst) t)) \to
 160 (\forall (c2: C).((csub3 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1
 161 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 162 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 163 (u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 164 T).(ty3 g d2 u t)))))))))) with [(CSort n0) \Rightarrow (\lambda (_: (drop n
 165 O c1 (CSort n0))).(\lambda (H4: (clear (CSort n0) (CHead d1 (Bind Abst)
 166 t))).(clear_gen_sort (CHead d1 (Bind Abst) t) n0 H4 (\forall (c2: C).((csub3
 167 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 168 C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 169 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 170 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 171 t)))))))))) | (CHead c k t0) \Rightarrow (\lambda (H3: (drop n O c1 (CHead c
 172 k t0))).(\lambda (H4: (clear (CHead c k t0) (CHead d1 (Bind Abst)
 173 t))).((match k in K return (\lambda (k0: K).((drop n O c1 (CHead c k0 t0))
 174 \to ((clear (CHead c k0 t0) (CHead d1 (Bind Abst) t)) \to (\forall (c2:
 175 C).((csub3 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 176 (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 177 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 178 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 179 t)))))))))) with [(Bind b) \Rightarrow (\lambda (H5: (drop n O c1 (CHead c
 180 (Bind b) t0))).(\lambda (H6: (clear (CHead c (Bind b) t0) (CHead d1 (Bind
 181 Abst) t))).(let H7 \def (f_equal C C (\lambda (e: C).(match e in C return
 182 (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c0 _ _)
 183 \Rightarrow c0])) (CHead d1 (Bind Abst) t) (CHead c (Bind b) t0)
 184 (clear_gen_bind b c (CHead d1 (Bind Abst) t) t0 H6)) in ((let H8 \def
 185 (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
 186 [(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 in K
 187 return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
 188 \Rightarrow Abst])])) (CHead d1 (Bind Abst) t) (CHead c (Bind b) t0)
 189 (clear_gen_bind b c (CHead d1 (Bind Abst) t) t0 H6)) in ((let H9 \def
 190 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 191 [(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1])) (CHead d1 (Bind
 192 Abst) t) (CHead c (Bind b) t0) (clear_gen_bind b c (CHead d1 (Bind Abst) t)
 193 t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1 c)).(\lambda
 194 (c2: C).(\lambda (H12: (csub3 g c1 c2)).(let H13 \def (eq_ind_r T t0 (\lambda
 195 (t1: T).(drop n O c1 (CHead c (Bind b) t1))) H5 t H9) in (let H14 \def
 196 (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead c (Bind b0) t))) H13 Abst
 197 H10) in (let H15 \def (eq_ind_r C c (\lambda (c0: C).(drop n O c1 (CHead c0
 198 (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C (\lambda (d2: C).(csub3 g d1
 199 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 200 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 201 (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 202 T).(ty3 g d2 u t)))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 203 (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 204 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 205 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 206 t))))) (\lambda (H16: (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 207 C).(drop n O c2 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2:
 208 C).(csub3 g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t)))
 209 (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n c2
 210 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 211 T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n c2 (CHead d2
 212 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 213 (\lambda (x0: C).(\lambda (H17: (csub3 g d1 x0)).(\lambda (H18: (drop n O c2
 214 (CHead x0 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csub3 g d1
 215 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 216 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 217 (u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 218 T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 219 (d2: C).(getl n c2 (CHead d2 (Bind Abst) t))) x0 H17 (getl_intro n c2 (CHead
 220 x0 (Bind Abst) t) (CHead x0 (Bind Abst) t) H18 (clear_bind Abst x0 t)))))))
 221 H16)) (\lambda (H16: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1
 222 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr)
 223 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex3_2_ind C T
 224 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 225 (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 226 T).(ty3 g d2 u t))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 227 (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 228 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 229 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 230 t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H17: (csub3 g d1
 231 x0)).(\lambda (H18: (drop n O c2 (CHead x0 (Bind Abbr) x1))).(\lambda (H19:
 232 (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 233 (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 234 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
 235 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 236 t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2)))
 237 (\lambda (d2: C).(\lambda (u: T).(getl n c2 (CHead d2 (Bind Abbr) u))))
 238 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) x0 x1 H17 (getl_intro n c2
 239 (CHead x0 (Bind Abbr) x1) (CHead x0 (Bind Abbr) x1) H18 (clear_bind Abbr x0
 240 x1)) H19))))))) H16)) (csub3_drop_abst g n c1 c2 H12 d1 t H15)))))))))) H8))
 241 H7)))) | (Flat f) \Rightarrow (\lambda (H5: (drop n O c1 (CHead c (Flat f)
 242 t0))).(\lambda (H6: (clear (CHead c (Flat f) t0) (CHead d1 (Bind Abst)
 243 t))).(let H7 \def H5 in (unintro C c1 (\lambda (c0: C).((drop n O c0 (CHead c
 244 (Flat f) t0)) \to (\forall (c2: C).((csub3 g c0 c2) \to (or (ex2 C (\lambda
 245 (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst)
 246 t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda
 247 (d2: C).(\lambda (u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
 248 C).(\lambda (u: T).(ty3 g d2 u t))))))))) (nat_ind (\lambda (n0:
 249 nat).(\forall (x0: C).((drop n0 O x0 (CHead c (Flat f) t0)) \to (\forall (c2:
 250 C).((csub3 g x0 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 251 (d2: C).(getl n0 c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 252 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl
 253 n0 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2
 254 u t)))))))))) (\lambda (x0: C).(\lambda (H8: (drop O O x0 (CHead c (Flat f)
 255 t0))).(\lambda (c2: C).(\lambda (H9: (csub3 g x0 c2)).(let H10 \def (eq_ind C
 256 x0 (\lambda (c0: C).(csub3 g c0 c2)) H9 (CHead c (Flat f) t0) (drop_gen_refl
 257 x0 (CHead c (Flat f) t0) H8)) in (let H_y \def (clear_flat c (CHead d1 (Bind
 258 Abst) t) (clear_gen_flat f c (CHead d1 (Bind Abst) t) t0 H6) f t0) in (let
 259 H11 \def (csub3_clear_conf g (CHead c (Flat f) t0) c2 H10 (CHead d1 (Bind
 260 Abst) t) H_y) in (ex2_ind C (\lambda (e2: C).(csub3 g (CHead d1 (Bind Abst)
 261 t) e2)) (\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(csub3 g
 262 d1 d2)) (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 263 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 264 (u: T).(getl O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 265 T).(ty3 g d2 u t))))) (\lambda (x1: C).(\lambda (H12: (csub3 g (CHead d1
 266 (Bind Abst) t) x1)).(\lambda (H13: (clear c2 x1)).(let H14 \def
 267 (csub3_gen_abst g d1 x1 t H12) in (or_ind (ex2 C (\lambda (e2: C).(eq C x1
 268 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csub3 g d1 e2))) (ex3_2 C T
 269 (\lambda (e2: C).(\lambda (v2: T).(eq C x1 (CHead e2 (Bind Abbr) v2))))
 270 (\lambda (e2: C).(\lambda (_: T).(csub3 g d1 e2))) (\lambda (e2: C).(\lambda
 271 (v2: T).(ty3 g e2 v2 t)))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2))
 272 (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
 273 (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u:
 274 T).(getl O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 275 T).(ty3 g d2 u t))))) (\lambda (H15: (ex2 C (\lambda (e2: C).(eq C x1 (CHead
 276 e2 (Bind Abst) t))) (\lambda (e2: C).(csub3 g d1 e2)))).(ex2_ind C (\lambda
 277 (e2: C).(eq C x1 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csub3 g d1 e2))
 278 (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl O c2
 279 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 280 T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl O c2 (CHead d2
 281 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 282 (\lambda (x2: C).(\lambda (H16: (eq C x1 (CHead x2 (Bind Abst) t))).(\lambda
 283 (H17: (csub3 g d1 x2)).(let H18 \def (eq_ind C x1 (\lambda (c0: C).(clear c2
 284 c0)) H13 (CHead x2 (Bind Abst) t) H16) in (or_introl (ex2 C (\lambda (d2:
 285 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) t))))
 286 (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2:
 287 C).(\lambda (u: T).(getl O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2:
 288 C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csub3 g
 289 d1 d2)) (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) t))) x2 H17
 290 (getl_intro O c2 (CHead x2 (Bind Abst) t) c2 (drop_refl c2) H18))))))) H15))
 291 (\lambda (H15: (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C x1 (CHead
 292 e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g d1 e2)))
 293 (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))))).(ex3_2_ind C T (\lambda
 294 (e2: C).(\lambda (v2: T).(eq C x1 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
 295 C).(\lambda (_: T).(csub3 g d1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
 296 e2 v2 t))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 297 C).(getl O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 298 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl O
 299 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 300 t))))) (\lambda (x2: C).(\lambda (x3: T).(\lambda (H16: (eq C x1 (CHead x2
 301 (Bind Abbr) x3))).(\lambda (H17: (csub3 g d1 x2)).(\lambda (H18: (ty3 g x2 x3
 302 t)).(let H19 \def (eq_ind C x1 (\lambda (c0: C).(clear c2 c0)) H13 (CHead x2
 303 (Bind Abbr) x3) H16) in (or_intror (ex2 C (\lambda (d2: C).(csub3 g d1 d2))
 304 (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda
 305 (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u:
 306 T).(getl O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 307 T).(ty3 g d2 u t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csub3
 308 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl O c2 (CHead d2 (Bind Abbr)
 309 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) x2 x3 H17 (getl_intro
 310 O c2 (CHead x2 (Bind Abbr) x3) c2 (drop_refl c2) H19) H18)))))))) H15))
 311 H14))))) H11)))))))) (\lambda (n0: nat).(\lambda (H8: ((\forall (x0:
 312 C).((drop n0 O x0 (CHead c (Flat f) t0)) \to (\forall (c2: C).((csub3 g x0
 313 c2) \to (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl
 314 n0 c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 315 T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n0 c2 (CHead d2
 316 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 317 t))))))))))).(\lambda (x0: C).(\lambda (H9: (drop (S n0) O x0 (CHead c (Flat
 318 f) t0))).(\lambda (c2: C).(\lambda (H10: (csub3 g x0 c2)).(let H11 \def
 319 (drop_clear x0 (CHead c (Flat f) t0) n0 H9) in (ex2_3_ind B C T (\lambda (b:
 320 B).(\lambda (e: C).(\lambda (v: T).(clear x0 (CHead e (Bind b) v)))))
 321 (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop n0 O e (CHead c (Flat
 322 f) t0))))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 323 C).(getl (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 324 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl
 325 (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 326 d2 u t))))) (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H12:
 327 (clear x0 (CHead x2 (Bind x1) x3))).(\lambda (H13: (drop n0 O x2 (CHead c
 328 (Flat f) t0))).(let H14 \def (csub3_clear_conf g x0 c2 H10 (CHead x2 (Bind
 329 x1) x3) H12) in (ex2_ind C (\lambda (e2: C).(csub3 g (CHead x2 (Bind x1) x3)
 330 e2)) (\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(csub3 g d1
 331 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 332 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 333 (u: T).(getl (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda
 334 (u: T).(ty3 g d2 u t))))) (\lambda (x4: C).(\lambda (H15: (csub3 g (CHead x2
 335 (Bind x1) x3) x4)).(\lambda (H16: (clear c2 x4)).(let H17 \def
 336 (csub3_gen_bind g x1 x2 x4 x3 H15) in (ex2_3_ind B C T (\lambda (b2:
 337 B).(\lambda (e2: C).(\lambda (v2: T).(eq C x4 (CHead e2 (Bind b2) v2)))))
 338 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g x2 e2)))) (or (ex2
 339 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead
 340 d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1
 341 d2))) (\lambda (d2: C).(\lambda (u: T).(getl (S n0) c2 (CHead d2 (Bind Abbr)
 342 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x5:
 343 B).(\lambda (x6: C).(\lambda (x7: T).(\lambda (H18: (eq C x4 (CHead x6 (Bind
 344 x5) x7))).(\lambda (H19: (csub3 g x2 x6)).(let H20 \def (eq_ind C x4 (\lambda
 345 (c0: C).(clear c2 c0)) H16 (CHead x6 (Bind x5) x7) H18) in (let H21 \def (H8
 346 x2 H13 x6 H19) in (or_ind (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 347 (d2: C).(getl n0 x6 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 348 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl
 349 n0 x6 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2
 350 u t)))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl
 351 (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda
 352 (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl (S n0) c2
 353 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
 354 t))))) (\lambda (H22: (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2:
 355 C).(getl n0 x6 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2:
 356 C).(csub3 g d1 d2)) (\lambda (d2: C).(getl n0 x6 (CHead d2 (Bind Abst) t)))
 357 (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda (d2: C).(getl (S n0) c2
 358 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2: C).(\lambda (_:
 359 T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl (S n0) c2 (CHead
 360 d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
 361 (\lambda (x8: C).(\lambda (H23: (csub3 g d1 x8)).(\lambda (H24: (getl n0 x6
 362 (CHead x8 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csub3 g d1
 363 d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T
 364 (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda
 365 (u: T).(getl (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda
 366 (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csub3 g d1 d2))
 367 (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abst) t))) x8 H23
 368 (getl_clear_bind x5 c2 x6 x7 H20 (CHead x8 (Bind Abst) t) n0 H24)))))) H22))
 369 (\lambda (H22: (ex3_2 C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1 d2)))
 370 (\lambda (d2: C).(\lambda (u: T).(getl n0 x6 (CHead d2 (Bind Abbr) u))))
 371 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex3_2_ind C T (\lambda
 372 (d2: C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u:
 373 T).(getl n0 x6 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u:
 374 T).(ty3 g d2 u t))) (or (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 375 (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 376 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl
 377 (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 378 d2 u t))))) (\lambda (x8: C).(\lambda (x9: T).(\lambda (H23: (csub3 g d1
 379 x8)).(\lambda (H24: (getl n0 x6 (CHead x8 (Bind Abbr) x9))).(\lambda (H25:
 380 (ty3 g x8 x9 t)).(or_intror (ex2 C (\lambda (d2: C).(csub3 g d1 d2)) (\lambda
 381 (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abst) t)))) (ex3_2 C T (\lambda (d2:
 382 C).(\lambda (_: T).(csub3 g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl
 383 (S n0) c2 (CHead d2 (Bind Abbr) u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
 384 d2 u t)))) (ex3_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csub3 g d1
 385 d2))) (\lambda (d2: C).(\lambda (u: T).(getl (S n0) c2 (CHead d2 (Bind Abbr)
 386 u)))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) x8 x9 H23
 387 (getl_clear_bind x5 c2 x6 x7 H20 (CHead x8 (Bind Abbr) x9) n0 H24) H25)))))))
 388 H22)) H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))]) H3 H4)))]) H1
 389 H2)))) H0))))))).
 390