matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.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/LambdaDelta-1/ty3/pr3_props".
  18
  19 include "ty3/pr3.ma".
  20
  21 theorem ty3_cred_pr2:
  22  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1
  23 v2) \to (\forall (b: B).(\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c
  24 (Bind b) v1) t1 t2) \to (ty3 g (CHead c (Bind b) v2) t1 t2)))))))))
  25 \def
  26  \lambda (g: G).(\lambda (c: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda
  27 (H: (pr2 c v1 v2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
  28 T).(\forall (b: B).(\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c0 (Bind
  29 b) t) t1 t2) \to (ty3 g (CHead c0 (Bind b) t0) t1 t2)))))))) (\lambda (c0:
  30 C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr0 t1 t2)).(\lambda (b:
  31 B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H1: (ty3 g (CHead c0 (Bind b)
  32 t1) t0 t3)).(ty3_sred_wcpr0_pr0 g (CHead c0 (Bind b) t1) t0 t3 H1 (CHead c0
  33 (Bind b) t2) (wcpr0_comp c0 c0 (wcpr0_refl c0) t1 t2 H0 (Bind b)) t0
  34 (pr0_refl t0)))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
  35 T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr)
  36 u))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H1: (pr0 t1 t2)).(\lambda
  37 (t: T).(\lambda (H2: (subst0 i u t2 t)).(\lambda (b: B).(\lambda (t0:
  38 T).(\lambda (t3: T).(\lambda (H3: (ty3 g (CHead c0 (Bind b) t1) t0
  39 t3)).(ty3_csubst0 g (CHead c0 (Bind b) t2) t0 t3 (ty3_sred_wcpr0_pr0 g (CHead
  40 c0 (Bind b) t1) t0 t3 H3 (CHead c0 (Bind b) t2) (wcpr0_comp c0 c0 (wcpr0_refl
  41 c0) t1 t2 H1 (Bind b)) t0 (pr0_refl t0)) d u (S i) (getl_clear_bind b (CHead
  42 c0 (Bind b) t2) c0 t2 (clear_bind b c0 t2) (CHead d (Bind Abbr) u) i H0)
  43 (CHead c0 (Bind b) t) (csubst0_snd_bind b i u t2 t H2 c0)))))))))))))))) c v1
  44 v2 H))))).
  45
  46 theorem ty3_cred_pr3:
  47  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr3 c v1
  48 v2) \to (\forall (b: B).(\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c
  49 (Bind b) v1) t1 t2) \to (ty3 g (CHead c (Bind b) v2) t1 t2)))))))))
  50 \def
  51  \lambda (g: G).(\lambda (c: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda
  52 (H: (pr3 c v1 v2)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (b:
  53 B).(\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c (Bind b) t) t1 t2) \to
  54 (ty3 g (CHead c (Bind b) t0) t1 t2))))))) (\lambda (t: T).(\lambda (b:
  55 B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (ty3 g (CHead c (Bind b)
  56 t) t1 t2)).H0))))) (\lambda (t2: T).(\lambda (t1: T).(\lambda (H0: (pr2 c t1
  57 t2)).(\lambda (t3: T).(\lambda (_: (pr3 c t2 t3)).(\lambda (H2: ((\forall (b:
  58 B).(\forall (t4: T).(\forall (t5: T).((ty3 g (CHead c (Bind b) t2) t4 t5) \to
  59 (ty3 g (CHead c (Bind b) t3) t4 t5))))))).(\lambda (b: B).(\lambda (t0:
  60 T).(\lambda (t4: T).(\lambda (H3: (ty3 g (CHead c (Bind b) t1) t0 t4)).(H2 b
  61 t0 t4 (ty3_cred_pr2 g c t1 t2 H0 b t0 t4 H3)))))))))))) v1 v2 H))))).
  62
  63 theorem ty3_gen_lift:
  64  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h:
  65 nat).(\forall (d: nat).((ty3 g c (lift h d t1) x) \to (\forall (e: C).((drop
  66 h d c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2:
  67 T).(ty3 g e t1 t2)))))))))))
  68 \def
  69  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (x: T).(\lambda (h:
  70 nat).(\lambda (d: nat).(\lambda (H: (ty3 g c (lift h d t1) x)).(insert_eq T
  71 (lift h d t1) (\lambda (t: T).(ty3 g c t x)) (\forall (e: C).((drop h d c e)
  72 \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2: T).(ty3 g
  73 e t1 t2))))) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(unintro nat d
  74 (\lambda (n: nat).((eq T y (lift h n t1)) \to (\forall (e: C).((drop h n c e)
  75 \to (ex2 T (\lambda (t2: T).(pc3 c (lift h n t2) x)) (\lambda (t2: T).(ty3 g
  76 e t1 t2))))))) (unintro T t1 (\lambda (t: T).(\forall (x0: nat).((eq T y
  77 (lift h x0 t)) \to (\forall (e: C).((drop h x0 c e) \to (ex2 T (\lambda (t2:
  78 T).(pc3 c (lift h x0 t2) x)) (\lambda (t2: T).(ty3 g e t t2)))))))) (ty3_ind
  79 g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall
  80 (x1: nat).((eq T t (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
  81 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) t0)) (\lambda (t2: T).(ty3 g e
  82 x0 t2))))))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t: T).(\lambda
  83 (_: (ty3 g c0 t2 t)).(\lambda (_: ((\forall (x0: T).(\forall (x1: nat).((eq T
  84 t2 (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda
  85 (t3: T).(pc3 c0 (lift h x1 t3) t)) (\lambda (t3: T).(ty3 g e x0
  86 t3)))))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u
  87 t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1
  88 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t4: T).(pc3
  89 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda
  90 (H5: (pc3 c0 t3 t2)).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H6: (eq T
  91 u (lift h x1 x0))).(\lambda (e: C).(\lambda (H7: (drop h x1 c0 e)).(let H8
  92 \def (eq_ind T u (\lambda (t0: T).(\forall (x2: T).(\forall (x3: nat).((eq T
  93 t0 (lift h x3 x2)) \to (\forall (e0: C).((drop h x3 c0 e0) \to (ex2 T
  94 (\lambda (t4: T).(pc3 c0 (lift h x3 t4) t3)) (\lambda (t4: T).(ty3 g e0 x2
  95 t4))))))))) H4 (lift h x1 x0) H6) in (let H9 \def (eq_ind T u (\lambda (t0:
  96 T).(ty3 g c0 t0 t3)) H3 (lift h x1 x0) H6) in (let H10 \def (H8 x0 x1
  97 (refl_equal T (lift h x1 x0)) e H7) in (ex2_ind T (\lambda (t4: T).(pc3 c0
  98 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)) (ex2 T (\lambda (t4:
  99 T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: T).(ty3 g e x0 t4))) (\lambda
 100 (x2: T).(\lambda (H11: (pc3 c0 (lift h x1 x2) t3)).(\lambda (H12: (ty3 g e x0
 101 x2)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4:
 102 T).(ty3 g e x0 t4)) x2 (pc3_t t3 c0 (lift h x1 x2) H11 t2 H5) H12))))
 103 H10))))))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (x0:
 104 T).(\lambda (x1: nat).(\lambda (H1: (eq T (TSort m) (lift h x1 x0))).(\lambda
 105 (e: C).(\lambda (_: (drop h x1 c0 e)).(eq_ind_r T (TSort m) (\lambda (t:
 106 T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (TSort (next g m))))
 107 (\lambda (t2: T).(ty3 g e t t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0
 108 (lift h x1 t2) (TSort (next g m)))) (\lambda (t2: T).(ty3 g e (TSort m) t2))
 109 (TSort (next g m)) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(pc3 c0 t
 110 (TSort (next g m)))) (pc3_refl c0 (TSort (next g m))) (lift h x1 (TSort (next
 111 g m))) (lift_sort (next g m) h x1)) (ty3_sort g e m)) x0 (lift_gen_sort h x1
 112 m x0 H1))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d0: C).(\lambda
 113 (u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind Abbr) u))).(\lambda (t:
 114 T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3: ((\forall (x0: T).(\forall
 115 (x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 d0 e) \to
 116 (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e
 117 x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T
 118 (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda (H5: (drop h x1 c0
 119 e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6 \def H_x in (or_ind
 120 (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 h) n) (eq T x0 (TLRef
 121 (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O
 122 t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: (land (lt n x1) (eq T
 123 x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) (ex2 T (\lambda (t2:
 124 T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0
 125 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 (TLRef n))).(eq_ind_r T
 126 (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
 127 (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind
 128 nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 (S (plus n (minus x1 (S n))))
 129 (lt_plus_minus n x1 H8)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
 130 C).(eq T u (lift h (minus x1 (S n)) v)))) (\lambda (v: T).(\lambda (e0:
 131 C).(getl n e (CHead e0 (Bind Abbr) v)))) (\lambda (_: T).(\lambda (e0:
 132 C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
 133 x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda
 134 (x2: T).(\lambda (x3: C).(\lambda (H11: (eq T u (lift h (minus x1 (S n))
 135 x2))).(\lambda (H12: (getl n e (CHead x3 (Bind Abbr) x2))).(\lambda (H13:
 136 (drop h (minus x1 (S n)) d0 x3)).(let H14 \def (eq_ind T u (\lambda (t0:
 137 T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall
 138 (e0: C).((drop h x5 d0 e0) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x5 t2)
 139 t)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H3 (lift h (minus x1 (S n)) x2)
 140 H11) in (let H15 \def (eq_ind T u (\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift
 141 h (minus x1 (S n)) x2) H11) in (let H16 \def (H14 x2 (minus x1 (S n))
 142 (refl_equal T (lift h (minus x1 (S n)) x2)) x3 H13) in (ex2_ind T (\lambda
 143 (t2: T).(pc3 d0 (lift h (minus x1 (S n)) t2) t)) (\lambda (t2: T).(ty3 g x3
 144 x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t)))
 145 (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda (x4: T).(\lambda (H17:
 146 (pc3 d0 (lift h (minus x1 (S n)) x4) t)).(\lambda (H18: (ty3 g x3 x2
 147 x4)).(eq_ind_r nat (plus (S n) (minus x1 (S n))) (\lambda (n0: nat).(ex2 T
 148 (\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift (S n) O t))) (\lambda (t2:
 149 T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h
 150 (plus (S n) (minus x1 (S n))) t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g
 151 e (TLRef n) t2)) (lift (S n) O x4) (eq_ind_r T (lift (S n) O (lift h (minus
 152 x1 (S n)) x4)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O t))) (pc3_lift c0 d0
 153 (S n) O (getl_drop Abbr c0 d0 u n H1) (lift h (minus x1 (S n)) x4) t H17)
 154 (lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)) (lift_d x4 h (S n)
 155 (minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abbr g n e x3 x2 H12 x4
 156 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16))))))))) (getl_drop_conf_lt Abbr
 157 c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land
 158 (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h)
 159 n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1
 160 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le
 161 (plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T
 162 (TLRef (minus n h)) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h
 163 x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (ex_intro2 T
 164 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2:
 165 T).(ty3 g e (TLRef (minus n h)) t2)) (lift (S (minus n h)) O t) (eq_ind_r T
 166 (lift (plus h (S (minus n h))) O t) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O
 167 t))) (eq_ind nat (S (plus h (minus n h))) (\lambda (n0: nat).(pc3 c0 (lift n0
 168 O t) (lift (S n) O t))) (eq_ind nat n (\lambda (n0: nat).(pc3 c0 (lift (S n0)
 169 O t) (lift (S n) O t))) (pc3_refl c0 (lift (S n) O t)) (plus h (minus n h))
 170 (le_plus_minus h n (le_trans h (plus x1 h) n (le_plus_r x1 h) H8))) (plus h
 171 (S (minus n h))) (plus_n_Sm h (minus n h))) (lift h x1 (lift (S (minus n h))
 172 O t)) (lift_free t (S (minus n h)) h O x1 (le_trans x1 (S (minus n h)) (plus
 173 O (S (minus n h))) (le_S_minus x1 h n H8) (le_n (plus O (S (minus n h)))))
 174 (le_O_n x1))) (ty3_abbr g (minus n h) e d0 u (getl_drop_conf_ge n (CHead d0
 175 (Bind Abbr) u) c0 H1 e h x1 H5 H8) t H2)) x0 H9))) H7)) H6))))))))))))))))
 176 (\lambda (n: nat).(\lambda (c0: C).(\lambda (d0: C).(\lambda (u: T).(\lambda
 177 (H1: (getl n c0 (CHead d0 (Bind Abst) u))).(\lambda (t: T).(\lambda (H2: (ty3
 178 g d0 u t)).(\lambda (H3: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift
 179 h x1 x0)) \to (\forall (e: C).((drop h x1 d0 e) \to (ex2 T (\lambda (t2:
 180 T).(pc3 d0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e x0
 181 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T (TLRef
 182 n) (lift h x1 x0))).(\lambda (e: C).(\lambda (H5: (drop h x1 c0 e)).(let H_x
 183 \def (lift_gen_lref x0 x1 h n H4) in (let H6 \def H_x in (or_ind (land (lt n
 184 x1) (eq T x0 (TLRef n))) (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n
 185 h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u)))
 186 (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: (land (lt n x1) (eq T x0
 187 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) (ex2 T (\lambda (t2:
 188 T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0
 189 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 (TLRef n))).(eq_ind_r T
 190 (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
 191 (lift (S n) O u))) (\lambda (t2: T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind
 192 nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 (S (plus n (minus x1 (S n))))
 193 (lt_plus_minus n x1 H8)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
 194 C).(eq T u (lift h (minus x1 (S n)) v)))) (\lambda (v: T).(\lambda (e0:
 195 C).(getl n e (CHead e0 (Bind Abst) v)))) (\lambda (_: T).(\lambda (e0:
 196 C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h
 197 x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda
 198 (x2: T).(\lambda (x3: C).(\lambda (H11: (eq T u (lift h (minus x1 (S n))
 199 x2))).(\lambda (H12: (getl n e (CHead x3 (Bind Abst) x2))).(\lambda (H13:
 200 (drop h (minus x1 (S n)) d0 x3)).(let H14 \def (eq_ind T u (\lambda (t0:
 201 T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall
 202 (e0: C).((drop h x5 d0 e0) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x5 t2)
 203 t)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H3 (lift h (minus x1 (S n)) x2)
 204 H11) in (let H15 \def (eq_ind T u (\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift
 205 h (minus x1 (S n)) x2) H11) in (eq_ind_r T (lift h (minus x1 (S n)) x2)
 206 (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O
 207 t0))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))) (let H16 \def (H14 x2 (minus
 208 x1 (S n)) (refl_equal T (lift h (minus x1 (S n)) x2)) x3 H13) in (ex2_ind T
 209 (\lambda (t2: T).(pc3 d0 (lift h (minus x1 (S n)) t2) t)) (\lambda (t2:
 210 T).(ty3 g x3 x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S
 211 n) O (lift h (minus x1 (S n)) x2)))) (\lambda (t2: T).(ty3 g e (TLRef n)
 212 t2))) (\lambda (x4: T).(\lambda (_: (pc3 d0 (lift h (minus x1 (S n)) x4)
 213 t)).(\lambda (H18: (ty3 g x3 x2 x4)).(eq_ind_r nat (plus (S n) (minus x1 (S
 214 n))) (\lambda (n0: nat).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift
 215 (S n) O (lift h (minus n0 (S n)) x2)))) (\lambda (t2: T).(ty3 g e (TLRef n)
 216 t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h (plus (S n) (minus x1 (S
 217 n))) t2) (lift (S n) O (lift h (minus (plus (S n) (minus x1 (S n))) (S n))
 218 x2)))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)) (lift (S n) O x2) (eq_ind_r T
 219 (lift (S n) O (lift h (minus x1 (S n)) x2)) (\lambda (t0: T).(pc3 c0 t0 (lift
 220 (S n) O (lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2)))) (eq_ind
 221 nat x1 (\lambda (n0: nat).(pc3 c0 (lift (S n) O (lift h (minus x1 (S n)) x2))
 222 (lift (S n) O (lift h (minus n0 (S n)) x2)))) (pc3_refl c0 (lift (S n) O
 223 (lift h (minus x1 (S n)) x2))) (plus (S n) (minus x1 (S n))) (le_plus_minus
 224 (S n) x1 H8)) (lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x2))
 225 (lift_d x2 h (S n) (minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abst g
 226 n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16)) u H11))))))))
 227 (getl_drop_conf_lt Abst c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9)))
 228 H7)) (\lambda (H7: (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n
 229 h))))).(and_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T
 230 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2:
 231 T).(ty3 g e x0 t2))) (\lambda (H8: (le (plus x1 h) n)).(\lambda (H9: (eq T x0
 232 (TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n h)) (\lambda (t0: T).(ex2 T
 233 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2:
 234 T).(ty3 g e t0 t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
 235 (lift (S n) O u))) (\lambda (t2: T).(ty3 g e (TLRef (minus n h)) t2)) (lift
 236 (S (minus n h)) O u) (eq_ind_r T (lift (plus h (S (minus n h))) O u) (\lambda
 237 (t0: T).(pc3 c0 t0 (lift (S n) O u))) (eq_ind nat (S (plus h (minus n h)))
 238 (\lambda (n0: nat).(pc3 c0 (lift n0 O u) (lift (S n) O u))) (eq_ind nat n
 239 (\lambda (n0: nat).(pc3 c0 (lift (S n0) O u) (lift (S n) O u))) (pc3_refl c0
 240 (lift (S n) O u)) (plus h (minus n h)) (le_plus_minus h n (le_trans h (plus
 241 x1 h) n (le_plus_r x1 h) H8))) (plus h (S (minus n h))) (plus_n_Sm h (minus n
 242 h))) (lift h x1 (lift (S (minus n h)) O u)) (lift_free u (S (minus n h)) h O
 243 x1 (le_trans x1 (S (minus n h)) (plus O (S (minus n h))) (le_S_minus x1 h n
 244 H8) (le_n (plus O (S (minus n h))))) (le_O_n x1))) (ty3_abst g (minus n h) e
 245 d0 u (getl_drop_conf_ge n (CHead d0 (Bind Abst) u) c0 H1 e h x1 H5 H8) t H2))
 246 x0 H9))) H7)) H6)))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
 247 (t: T).(\lambda (H1: (ty3 g c0 u t)).(\lambda (H2: ((\forall (x0: T).(\forall
 248 (x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
 249 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e
 250 x0 t2)))))))))).(\lambda (b: B).(\lambda (t2: T).(\lambda (t3: T).(\lambda
 251 (H3: (ty3 g (CHead c0 (Bind b) u) t2 t3)).(\lambda (H4: ((\forall (x0:
 252 T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (\forall (e: C).((drop h
 253 x1 (CHead c0 (Bind b) u) e) \to (ex2 T (\lambda (t4: T).(pc3 (CHead c0 (Bind
 254 b) u) (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda
 255 (t0: T).(\lambda (H5: (ty3 g (CHead c0 (Bind b) u) t3 t0)).(\lambda (H6:
 256 ((\forall (x0: T).(\forall (x1: nat).((eq T t3 (lift h x1 x0)) \to (\forall
 257 (e: C).((drop h x1 (CHead c0 (Bind b) u) e) \to (ex2 T (\lambda (t4: T).(pc3
 258 (CHead c0 (Bind b) u) (lift h x1 t4) t0)) (\lambda (t4: T).(ty3 g e x0
 259 t4)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H7: (eq T (THead
 260 (Bind b) u t2) (lift h x1 x0))).(\lambda (e: C).(\lambda (H8: (drop h x1 c0
 261 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind b)
 262 y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u (lift h x1 y0)))) (\lambda
 263 (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda (t4:
 264 T).(pc3 c0 (lift h x1 t4) (THead (Bind b) u t3))) (\lambda (t4: T).(ty3 g e
 265 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H9: (eq T x0 (THead
 266 (Bind b) x2 x3))).(\lambda (H10: (eq T u (lift h x1 x2))).(\lambda (H11: (eq
 267 T t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind b) x2 x3) (\lambda (t4:
 268 T).(ex2 T (\lambda (t5: T).(pc3 c0 (lift h x1 t5) (THead (Bind b) u t3)))
 269 (\lambda (t5: T).(ty3 g e t4 t5)))) (let H12 \def (eq_ind T t2 (\lambda (t4:
 270 T).(\forall (x4: T).(\forall (x5: nat).((eq T t4 (lift h x5 x4)) \to (\forall
 271 (e0: C).((drop h x5 (CHead c0 (Bind b) u) e0) \to (ex2 T (\lambda (t5:
 272 T).(pc3 (CHead c0 (Bind b) u) (lift h x5 t5) t3)) (\lambda (t5: T).(ty3 g e0
 273 x4 t5))))))))) H4 (lift h (S x1) x3) H11) in (let H13 \def (eq_ind T t2
 274 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t4 t3)) H3 (lift h (S x1) x3)
 275 H11) in (let H14 \def (eq_ind T u (\lambda (t4: T).(ty3 g (CHead c0 (Bind b)
 276 t4) (lift h (S x1) x3) t3)) H13 (lift h x1 x2) H10) in (let H15 \def (eq_ind
 277 T u (\lambda (t4: T).(\forall (x4: T).(\forall (x5: nat).((eq T (lift h (S
 278 x1) x3) (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 (CHead c0 (Bind b)
 279 t4) e0) \to (ex2 T (\lambda (t5: T).(pc3 (CHead c0 (Bind b) t4) (lift h x5
 280 t5) t3)) (\lambda (t5: T).(ty3 g e0 x4 t5))))))))) H12 (lift h x1 x2) H10) in
 281 (let H16 \def (eq_ind T u (\lambda (t4: T).(\forall (x4: T).(\forall (x5:
 282 nat).((eq T t3 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 (CHead c0
 283 (Bind b) t4) e0) \to (ex2 T (\lambda (t5: T).(pc3 (CHead c0 (Bind b) t4)
 284 (lift h x5 t5) t0)) (\lambda (t5: T).(ty3 g e0 x4 t5))))))))) H6 (lift h x1
 285 x2) H10) in (let H17 \def (eq_ind T u (\lambda (t4: T).(ty3 g (CHead c0 (Bind
 286 b) t4) t3 t0)) H5 (lift h x1 x2) H10) in (let H18 \def (eq_ind T u (\lambda
 287 (t4: T).(\forall (x4: T).(\forall (x5: nat).((eq T t4 (lift h x5 x4)) \to
 288 (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t5: T).(pc3 c0 (lift
 289 h x5 t5) t)) (\lambda (t5: T).(ty3 g e0 x4 t5))))))))) H2 (lift h x1 x2) H10)
 290 in (let H19 \def (eq_ind T u (\lambda (t4: T).(ty3 g c0 t4 t)) H1 (lift h x1
 291 x2) H10) in (eq_ind_r T (lift h x1 x2) (\lambda (t4: T).(ex2 T (\lambda (t5:
 292 T).(pc3 c0 (lift h x1 t5) (THead (Bind b) t4 t3))) (\lambda (t5: T).(ty3 g e
 293 (THead (Bind b) x2 x3) t5)))) (let H20 \def (H18 x2 x1 (refl_equal T (lift h
 294 x1 x2)) e H8) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t))
 295 (\lambda (t4: T).(ty3 g e x2 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1
 296 t4) (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e (THead
 297 (Bind b) x2 x3) t4))) (\lambda (x4: T).(\lambda (_: (pc3 c0 (lift h x1 x4)
 298 t)).(\lambda (H22: (ty3 g e x2 x4)).(let H23 \def (H15 x3 (S x1) (refl_equal
 299 T (lift h (S x1) x3)) (CHead e (Bind b) x2) (drop_skip_bind h x1 c0 e H8 b
 300 x2)) in (ex2_ind T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) (lift h x1 x2))
 301 (lift h (S x1) t4) t3)) (\lambda (t4: T).(ty3 g (CHead e (Bind b) x2) x3 t4))
 302 (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2)
 303 t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4))) (\lambda (x5:
 304 T).(\lambda (H24: (pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h (S x1) x5)
 305 t3)).(\lambda (H25: (ty3 g (CHead e (Bind b) x2) x3 x5)).(ex_ind T (\lambda
 306 (t4: T).(ty3 g (CHead e (Bind b) x2) x5 t4)) (ex2 T (\lambda (t4: T).(pc3 c0
 307 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e
 308 (THead (Bind b) x2 x3) t4))) (\lambda (x6: T).(\lambda (H26: (ty3 g (CHead e
 309 (Bind b) x2) x5 x6)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4)
 310 (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e (THead (Bind
 311 b) x2 x3) t4)) (THead (Bind b) x2 x5) (eq_ind_r T (THead (Bind b) (lift h x1
 312 x2) (lift h (S x1) x5)) (\lambda (t4: T).(pc3 c0 t4 (THead (Bind b) (lift h
 313 x1 x2) t3))) (pc3_head_2 c0 (lift h x1 x2) (lift h (S x1) x5) t3 (Bind b)
 314 H24) (lift h x1 (THead (Bind b) x2 x5)) (lift_bind b x2 x5 h x1)) (ty3_bind g
 315 e x2 x4 H22 b x3 x5 H25 x6 H26)))) (ty3_correct g (CHead e (Bind b) x2) x3 x5
 316 H25))))) H23))))) H20)) u H10))))))))) x0 H9)))))) (lift_gen_bind b u t2 x0 h
 317 x1 H7)))))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u:
 318 T).(\lambda (H1: (ty3 g c0 w u)).(\lambda (H2: ((\forall (x0: T).(\forall
 319 (x1: nat).((eq T w (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
 320 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e
 321 x0 t2)))))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 v
 322 (THead (Bind Abst) u t))).(\lambda (H4: ((\forall (x0: T).(\forall (x1:
 323 nat).((eq T v (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2
 324 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Bind Abst) u t))) (\lambda
 325 (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda
 326 (H5: (eq T (THead (Flat Appl) w v) (lift h x1 x0))).(\lambda (e: C).(\lambda
 327 (H6: (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T
 328 x0 (THead (Flat Appl) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T w (lift
 329 h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T v (lift h x1 z)))) (ex2 T
 330 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind
 331 Abst) u t)))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (x2: T).(\lambda
 332 (x3: T).(\lambda (H7: (eq T x0 (THead (Flat Appl) x2 x3))).(\lambda (H8: (eq
 333 T w (lift h x1 x2))).(\lambda (H9: (eq T v (lift h x1 x3))).(eq_ind_r T
 334 (THead (Flat Appl) x2 x3) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0
 335 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t)))) (\lambda (t2:
 336 T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind T v (\lambda (t0: T).(\forall
 337 (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall (e0:
 338 C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x5 t2)
 339 (THead (Bind Abst) u t))) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H4 (lift
 340 h x1 x3) H9) in (let H11 \def (eq_ind T v (\lambda (t0: T).(ty3 g c0 t0
 341 (THead (Bind Abst) u t))) H3 (lift h x1 x3) H9) in (let H12 \def (eq_ind T w
 342 (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5
 343 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t2: T).(pc3
 344 c0 (lift h x5 t2) u)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H2 (lift h x1
 345 x2) H8) in (let H13 \def (eq_ind T w (\lambda (t0: T).(ty3 g c0 t0 u)) H1
 346 (lift h x1 x2) H8) in (eq_ind_r T (lift h x1 x2) (\lambda (t0: T).(ex2 T
 347 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) t0 (THead (Bind
 348 Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2)))) (let
 349 H14 \def (H12 x2 x1 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T
 350 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e x2 t2))
 351 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1
 352 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl)
 353 x2 x3) t2))) (\lambda (x4: T).(\lambda (H15: (pc3 c0 (lift h x1 x4)
 354 u)).(\lambda (H16: (ty3 g e x2 x4)).(let H17 \def (H10 x3 x1 (refl_equal T
 355 (lift h x1 x3)) e H6) in (ex2_ind T (\lambda (t2: T).(pc3 c0 (lift h x1 t2)
 356 (THead (Bind Abst) u t))) (\lambda (t2: T).(ty3 g e x3 t2)) (ex2 T (\lambda
 357 (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind
 358 Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2)))
 359 (\lambda (x5: T).(\lambda (H18: (pc3 c0 (lift h x1 x5) (THead (Bind Abst) u
 360 t))).(\lambda (H19: (ty3 g e x3 x5)).(ex3_2_ind T T (\lambda (u1: T).(\lambda
 361 (t2: T).(pr3 e x5 (THead (Bind Abst) u1 t2)))) (\lambda (u1: T).(\lambda (_:
 362 T).(pr3 c0 u (lift h x1 u1)))) (\lambda (_: T).(\lambda (t2: T).(\forall (b:
 363 B).(\forall (u0: T).(pr3 (CHead c0 (Bind b) u0) t (lift h (S x1) t2))))))
 364 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1
 365 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl)
 366 x2 x3) t2))) (\lambda (x6: T).(\lambda (x7: T).(\lambda (H20: (pr3 e x5
 367 (THead (Bind Abst) x6 x7))).(\lambda (H21: (pr3 c0 u (lift h x1
 368 x6))).(\lambda (H22: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c0 (Bind
 369 b) u0) t (lift h (S x1) x7)))))).(ex_ind T (\lambda (t0: T).(ty3 g e x5 t0))
 370 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1
 371 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl)
 372 x2 x3) t2))) (\lambda (x8: T).(\lambda (H23: (ty3 g e x5 x8)).(ex4_3_ind T T
 373 T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 e (THead (Bind Abst)
 374 x6 t2) x8)))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g e x6
 375 t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead e (Bind
 376 Abst) x6) x7 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g
 377 (CHead e (Bind Abst) x6) t2 t3)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1
 378 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)))) (\lambda
 379 (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) (\lambda (x9: T).(\lambda
 380 (x10: T).(\lambda (x11: T).(\lambda (_: (pc3 e (THead (Bind Abst) x6 x9)
 381 x8)).(\lambda (H25: (ty3 g e x6 x10)).(\lambda (H26: (ty3 g (CHead e (Bind
 382 Abst) x6) x7 x9)).(\lambda (H27: (ty3 g (CHead e (Bind Abst) x6) x9
 383 x11)).(ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl)
 384 (lift h x1 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead
 385 (Flat Appl) x2 x3) t2)) (THead (Flat Appl) x2 (THead (Bind Abst) x6 x7))
 386 (eq_ind_r T (THead (Flat Appl) (lift h x1 x2) (lift h x1 (THead (Bind Abst)
 387 x6 x7))) (\lambda (t0: T).(pc3 c0 t0 (THead (Flat Appl) (lift h x1 x2) (THead
 388 (Bind Abst) u t)))) (pc3_thin_dx c0 (lift h x1 (THead (Bind Abst) x6 x7))
 389 (THead (Bind Abst) u t) (eq_ind_r T (THead (Bind Abst) (lift h x1 x6) (lift h
 390 (S x1) x7)) (\lambda (t0: T).(pc3 c0 t0 (THead (Bind Abst) u t)))
 391 (pc3_head_21 c0 (lift h x1 x6) u (pc3_pr3_x c0 (lift h x1 x6) u H21) (Bind
 392 Abst) (lift h (S x1) x7) t (pc3_pr3_x (CHead c0 (Bind Abst) (lift h x1 x6))
 393 (lift h (S x1) x7) t (H22 Abst (lift h x1 x6)))) (lift h x1 (THead (Bind
 394 Abst) x6 x7)) (lift_bind Abst x6 x7 h x1)) (lift h x1 x2) Appl) (lift h x1
 395 (THead (Flat Appl) x2 (THead (Bind Abst) x6 x7))) (lift_flat Appl x2 (THead
 396 (Bind Abst) x6 x7) h x1)) (ty3_appl g e x2 x6 (ty3_conv g e x6 x10 H25 x2 x4
 397 H16 (pc3_gen_lift c0 x4 x6 h x1 (pc3_t u c0 (lift h x1 x4) H15 (lift h x1 x6)
 398 (pc3_pr3_r c0 u (lift h x1 x6) H21)) e H6)) x3 x7 (ty3_conv g e (THead (Bind
 399 Abst) x6 x7) (THead (Bind Abst) x6 x9) (ty3_bind g e x6 x10 H25 Abst x7 x9
 400 H26 x11 H27) x3 x5 H19 (pc3_pr3_r e x5 (THead (Bind Abst) x6 x7)
 401 H20))))))))))) (ty3_gen_bind g Abst e x6 x7 x8 (ty3_sred_pr3 e x5 (THead
 402 (Bind Abst) x6 x7) H20 g x8 H23))))) (ty3_correct g e x3 x5 H19)))))))
 403 (pc3_gen_lift_abst c0 x5 t u h x1 H18 e H6))))) H17))))) H14)) w H8))))) x0
 404 H7)))))) (lift_gen_flat Appl w v x0 h x1 H5)))))))))))))))) (\lambda (c0:
 405 C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (ty3 g c0 t2 t3)).(\lambda
 406 (H2: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to
 407 (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h
 408 x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda (t0:
 409 T).(\lambda (H3: (ty3 g c0 t3 t0)).(\lambda (H4: ((\forall (x0: T).(\forall
 410 (x1: nat).((eq T t3 (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to
 411 (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t0)) (\lambda (t4: T).(ty3 g e
 412 x0 t4)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T
 413 (THead (Flat Cast) t3 t2) (lift h x1 x0))).(\lambda (e: C).(\lambda (H6:
 414 (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0
 415 (THead (Flat Cast) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T t3 (lift h
 416 x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T
 417 (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3))) (\lambda
 418 (t4: T).(ty3 g e x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq
 419 T x0 (THead (Flat Cast) x2 x3))).(\lambda (H8: (eq T t3 (lift h x1
 420 x2))).(\lambda (H9: (eq T t2 (lift h x1 x3))).(eq_ind_r T (THead (Flat Cast)
 421 x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead
 422 (Flat Cast) t0 t3))) (\lambda (t4: T).(ty3 g e t t4)))) (let H10 \def (eq_ind
 423 T t3 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5
 424 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3
 425 c0 (lift h x5 t4) t0)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H4 (lift h
 426 x1 x2) H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t t0)) H3
 427 (lift h x1 x2) H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(\forall
 428 (x4: T).(\forall (x5: nat).((eq T t2 (lift h x5 x4)) \to (\forall (e0:
 429 C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t))
 430 (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H2 (lift h x1 x2) H8) in (let H13
 431 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t2 t)) H1 (lift h x1 x2) H8) in
 432 (eq_ind_r T (lift h x1 x2) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0
 433 (lift h x1 t4) (THead (Flat Cast) t0 t))) (\lambda (t4: T).(ty3 g e (THead
 434 (Flat Cast) x2 x3) t4)))) (let H14 \def (eq_ind T t2 (\lambda (t: T).(ty3 g
 435 c0 t (lift h x1 x2))) H13 (lift h x1 x3) H9) in (let H15 \def (eq_ind T t2
 436 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5 x4))
 437 \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0
 438 (lift h x5 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H12
 439 (lift h x1 x3) H9) in (let H16 \def (H15 x3 x1 (refl_equal T (lift h x1 x3))
 440 e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (lift h x1 x2)))
 441 (\lambda (t4: T).(ty3 g e x3 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1
 442 t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda (t4: T).(ty3 g e (THead
 443 (Flat Cast) x2 x3) t4))) (\lambda (x4: T).(\lambda (H17: (pc3 c0 (lift h x1
 444 x4) (lift h x1 x2))).(\lambda (H18: (ty3 g e x3 x4)).(let H19 \def (H10 x2 x1
 445 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0
 446 (lift h x1 t4) t0)) (\lambda (t4: T).(ty3 g e x2 t4)) (ex2 T (\lambda (t4:
 447 T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda
 448 (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4))) (\lambda (x5: T).(\lambda
 449 (H20: (pc3 c0 (lift h x1 x5) t0)).(\lambda (H21: (ty3 g e x2 x5)).(ex_intro2
 450 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1
 451 x2)))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4)) (THead (Flat
 452 Cast) x5 x2) (eq_ind_r T (THead (Flat Cast) (lift h x1 x5) (lift h x1 x2))
 453 (\lambda (t: T).(pc3 c0 t (THead (Flat Cast) t0 (lift h x1 x2)))) (pc3_head_1
 454 c0 (lift h x1 x5) t0 H20 (Flat Cast) (lift h x1 x2)) (lift h x1 (THead (Flat
 455 Cast) x5 x2)) (lift_flat Cast x5 x2 h x1)) (ty3_cast g e x3 x2 (ty3_conv g e
 456 x2 x5 H21 x3 x4 H18 (pc3_gen_lift c0 x4 x2 h x1 H17 e H6)) x5 H21)))))
 457 H19))))) H16)))) t3 H8))))) x0 H7)))))) (lift_gen_flat Cast t3 t2 x0 h x1
 458 H5))))))))))))))) c y x H0))))) H))))))).
 459
 460 theorem ty3_tred:
 461  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
 462 t1) \to (\forall (t2: T).((pr3 c t1 t2) \to (ty3 g c u t2)))))))
 463 \def
 464  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H:
 465 (ty3 g c u t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(ex_ind T
 466 (\lambda (t: T).(ty3 g c t1 t)) (ty3 g c u t2) (\lambda (x: T).(\lambda (H1:
 467 (ty3 g c t1 x)).(ty3_conv g c t2 x (ty3_sred_pr3 c t1 t2 H0 g x H1) u t1 H
 468 (pc3_pr3_r c t1 t2 H0)))) (ty3_correct g c u t1 H)))))))).
 469
 470 theorem ty3_sconv_pc3:
 471  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
 472 u1 t1) \to (\forall (u2: T).(\forall (t2: T).((ty3 g c u2 t2) \to ((pc3 c u1
 473 u2) \to (pc3 c t1 t2)))))))))
 474 \def
 475  \lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
 476 (H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
 477 u2 t2)).(\lambda (H1: (pc3 c u1 u2)).(let H2 \def H1 in (ex2_ind T (\lambda
 478 (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t)) (pc3 c t1 t2) (\lambda (x:
 479 T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(ty3_unique g c x
 480 t1 (ty3_sred_pr3 c u1 x H3 g t1 H) t2 (ty3_sred_pr3 c u2 x H4 g t2 H0)))))
 481 H2)))))))))).
 482
 483 theorem ty3_sred_back:
 484  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t0: T).((ty3 g c
 485 t1 t0) \to (\forall (t2: T).((pr3 c t1 t2) \to (\forall (t: T).((ty3 g c t2
 486 t) \to (ty3 g c t1 t)))))))))
 487 \def
 488  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t0: T).(\lambda
 489 (H: (ty3 g c t1 t0)).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(\lambda
 490 (t: T).(\lambda (H1: (ty3 g c t2 t)).(ex_ind T (\lambda (t3: T).(ty3 g c t
 491 t3)) (ty3 g c t1 t) (\lambda (x: T).(\lambda (H2: (ty3 g c t x)).(ty3_conv g
 492 c t x H2 t1 t0 H (ty3_unique g c t2 t0 (ty3_sred_pr3 c t1 t2 H0 g t0 H) t
 493 H1)))) (ty3_correct g c t2 t H1)))))))))).
 494
 495 theorem ty3_sconv:
 496  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
 497 u1 t1) \to (\forall (u2: T).(\forall (t2: T).((ty3 g c u2 t2) \to ((pc3 c u1
 498 u2) \to (ty3 g c u1 t2)))))))))
 499 \def
 500  \lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
 501 (H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
 502 u2 t2)).(\lambda (H1: (pc3 c u1 u2)).(let H2 \def H1 in (ex2_ind T (\lambda
 503 (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t)) (ty3 g c u1 t2) (\lambda
 504 (x: T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(ty3_sred_back
 505 g c u1 t1 H x H3 t2 (ty3_sred_pr3 c u2 x H4 g t2 H0))))) H2)))))))))).
 506