matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/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/props".
  18
  19 include "ty3/fwd.ma".
  20
  21 include "pc3/fwd.ma".
  22
  23 theorem ty3_lift:
  24  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e
  25 t1 t2) \to (\forall (c: C).(\forall (d: nat).(\forall (h: nat).((drop h d c
  26 e) \to (ty3 g c (lift h d t1) (lift h d t2))))))))))
  27 \def
  28  \lambda (g: G).(\lambda (e: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  29 (H: (ty3 g e t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda (t0:
  30 T).(\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
  31 (ty3 g c0 (lift h d t) (lift h d t0))))))))) (\lambda (c: C).(\lambda (t0:
  32 T).(\lambda (t: T).(\lambda (_: (ty3 g c t0 t)).(\lambda (H1: ((\forall (c0:
  33 C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h
  34 d t0) (lift h d t)))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (_: (ty3
  35 g c u t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
  36 nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
  37 t3)))))))).(\lambda (H4: (pc3 c t3 t0)).(\lambda (c0: C).(\lambda (d:
  38 nat).(\lambda (h: nat).(\lambda (H5: (drop h d c0 c)).(ty3_conv g c0 (lift h
  39 d t0) (lift h d t) (H1 c0 d h H5) (lift h d u) (lift h d t3) (H3 c0 d h H5)
  40 (pc3_lift c0 c h d H5 t3 t0 H4)))))))))))))))) (\lambda (c: C).(\lambda (m:
  41 nat).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (_: (drop
  42 h d c0 c)).(eq_ind_r T (TSort m) (\lambda (t: T).(ty3 g c0 t (lift h d (TSort
  43 (next g m))))) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(ty3 g c0
  44 (TSort m) t)) (ty3_sort g c0 m) (lift h d (TSort (next g m))) (lift_sort
  45 (next g m) h d)) (lift h d (TSort m)) (lift_sort m h d)))))))) (\lambda (n:
  46 nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
  47 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
  48 t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
  49 nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
  50 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
  51 (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
  52 (lift (S n) O t))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
  53 n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3 (CHead d (Bind Abbr) u) H0)
  54 in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0)))
  55 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n) e0 e1))) (\lambda (_:
  56 C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0
  57 (TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x0: C).(\lambda (x1:
  58 C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
  59 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind
  60 nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S
  61 n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0
  62 (S n)) H9 Abbr d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1
  63 (Bind Abbr) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h (minus d0
  64 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
  65 (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h (minus
  66 d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x d)).(eq_ind_r T
  67 (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t))))
  68 (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3 g c0 (TLRef
  69 n) (lift h n0 (lift (S n) O t)))) (eq_ind_r T (lift (S n) O (lift h (minus d0
  70 (S n)) t)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda
  71 (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))))
  72 (ty3_abbr g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0 (CHead x
  73 (Bind Abbr) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus d0 (S n))
  74 t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
  75 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
  76 n) O t)) (lift_d t h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
  77 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
  78 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
  79 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat
  80 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
  81 t)))) (eq_ind_r T (lift (plus h (S n)) O t) (\lambda (t0: T).(ty3 g c0 (TLRef
  82 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
  83 (TLRef (plus n h)) (lift n0 O t))) (ty3_abbr g (plus n h) c0 d u
  84 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) t H1) (plus
  85 h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
  86 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
  87 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
  88 (plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
  89 d0 H4)))))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d:
  90 C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda
  91 (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall
  92 (d0: nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u)
  93 (lift h d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h:
  94 nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0
  95 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5
  96 \def (drop_getl_trans_le n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3
  97 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_:
  98 C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n)
  99 e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst)
 100 u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda
 101 (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop
 102 h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let
 103 H9 \def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S
 104 (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0
 105 h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0
 106 (CHead c1 (Bind Abst) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h
 107 (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S
 108 n) O u))) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift
 109 h (minus d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x
 110 d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S
 111 n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3
 112 g c0 (TLRef n) (lift h n0 (lift (S n) O u)))) (eq_ind_r T (lift (S n) O (lift
 113 h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat
 114 d0 (\lambda (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S
 115 n)) u)))) (ty3_abst g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0
 116 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus
 117 d0 (S n)) t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
 118 (le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
 119 n) O u)) (lift_d u h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
 120 (le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
 121 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
 122 h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat
 123 (S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
 124 u)))) (eq_ind_r T (lift (plus h (S n)) O u) (\lambda (t0: T).(ty3 g c0 (TLRef
 125 (plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
 126 (TLRef (plus n h)) (lift n0 O u))) (ty3_abst g (plus n h) c0 d u
 127 (drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) t H1) (plus
 128 h (S n)) (plus_comm h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
 129 h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
 130 n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
 131 (plus n (S O)) (plus_comm n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
 132 d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t:
 133 T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
 134 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
 135 t)))))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3
 136 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
 137 nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
 138 (lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g
 139 (CHead c (Bind b) u) t3 t4)).(\lambda (H5: ((\forall (c0: C).(\forall (d:
 140 nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
 141 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d:
 142 nat).(\lambda (h: nat).(\lambda (H6: (drop h d c0 c)).(eq_ind_r T (THead
 143 (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t5: T).(ty3 g c0
 144 t5 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
 145 u) (lift h (s (Bind b) d) t3)) (\lambda (t5: T).(ty3 g c0 (THead (Bind b)
 146 (lift h d u) (lift h (s (Bind b) d) t0)) t5)) (ty3_bind g c0 (lift h d u)
 147 (lift h d t) (H1 c0 d h H6) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
 148 c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H6 b u)) (lift h
 149 (S d) t4) (H5 (CHead c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0
 150 c H6 b u))) (lift h d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d))
 151 (lift h d (THead (Bind b) u t0)) (lift_head (Bind b) u t0 h
 152 d))))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda
 153 (_: (ty3 g c w u)).(\lambda (H1: ((\forall (c0: C).(\forall (d: nat).(\forall
 154 (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d w) (lift h d
 155 u)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead
 156 (Bind Abst) u t))).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall
 157 (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d v) (lift h d (THead (Bind
 158 Abst) u t))))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h:
 159 nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead (Flat Appl) (lift h d
 160 w) (lift h (s (Flat Appl) d) v)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d
 161 (THead (Flat Appl) w (THead (Bind Abst) u t))))) (eq_ind_r T (THead (Flat
 162 Appl) (lift h d w) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t)))
 163 (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w) (lift h (s (Flat
 164 Appl) d) v)) t0)) (eq_ind_r T (THead (Bind Abst) (lift h (s (Flat Appl) d) u)
 165 (lift h (s (Bind Abst) (s (Flat Appl) d)) t)) (\lambda (t0: T).(ty3 g c0
 166 (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) (THead (Flat
 167 Appl) (lift h d w) t0))) (ty3_appl g c0 (lift h d w) (lift h d u) (H1 c0 d h
 168 H4) (lift h d v) (lift h (S d) t) (eq_ind T (lift h d (THead (Bind Abst) u
 169 t)) (\lambda (t0: T).(ty3 g c0 (lift h d v) t0)) (H3 c0 d h H4) (THead (Bind
 170 Abst) (lift h d u) (lift h (S d) t)) (lift_bind Abst u t h d))) (lift h (s
 171 (Flat Appl) d) (THead (Bind Abst) u t)) (lift_head (Bind Abst) u t h (s (Flat
 172 Appl) d))) (lift h d (THead (Flat Appl) w (THead (Bind Abst) u t)))
 173 (lift_head (Flat Appl) w (THead (Bind Abst) u t) h d)) (lift h d (THead (Flat
 174 Appl) w v)) (lift_head (Flat Appl) w v h d))))))))))))))) (\lambda (c:
 175 C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda
 176 (H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c)
 177 \to (ty3 g c0 (lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda
 178 (_: (ty3 g c t3 t4)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
 179 nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d
 180 t4)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4:
 181 (drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d t3) (lift h (s
 182 (Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d t3))) (ty3_cast g
 183 c0 (lift h (s (Flat Cast) d) t0) (lift h d t3) (H1 c0 d h H4) (lift h d t4)
 184 (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast)
 185 t3 t0 h d)))))))))))))) e t1 t2 H))))).
 186
 187 theorem ty3_correct:
 188  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
 189 t1 t2) \to (ex T (\lambda (t: T).(ty3 g c t2 t)))))))
 190 \def
 191  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 192 (H: (ty3 g c t1 t2)).(ty3_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda
 193 (t0: T).(ex T (\lambda (t3: T).(ty3 g c0 t0 t3)))))) (\lambda (c0:
 194 C).(\lambda (t0: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 t0 t)).(\lambda
 195 (_: (ex T (\lambda (t3: T).(ty3 g c0 t t3)))).(\lambda (u: T).(\lambda (t3:
 196 T).(\lambda (_: (ty3 g c0 u t3)).(\lambda (_: (ex T (\lambda (t4: T).(ty3 g
 197 c0 t3 t4)))).(\lambda (_: (pc3 c0 t3 t0)).(ex_intro T (\lambda (t4: T).(ty3 g
 198 c0 t0 t4)) t H0))))))))))) (\lambda (c0: C).(\lambda (m: nat).(ex_intro T
 199 (\lambda (t: T).(ty3 g c0 (TSort (next g m)) t)) (TSort (next g (next g m)))
 200 (ty3_sort g c0 (next g m))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
 201 C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr)
 202 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (H2: (ex T (\lambda
 203 (t0: T).(ty3 g d t t0)))).(let H3 \def H2 in (ex_ind T (\lambda (t0: T).(ty3
 204 g d t t0)) (ex T (\lambda (t0: T).(ty3 g c0 (lift (S n) O t) t0))) (\lambda
 205 (x: T).(\lambda (H4: (ty3 g d t x)).(ex_intro T (\lambda (t0: T).(ty3 g c0
 206 (lift (S n) O t) t0)) (lift (S n) O x) (ty3_lift g d t x H4 c0 O (S n)
 207 (getl_drop Abbr c0 d u n H0))))) H3)))))))))) (\lambda (n: nat).(\lambda (c0:
 208 C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind
 209 Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (_: (ex T
 210 (\lambda (t0: T).(ty3 g d t t0)))).(ex_intro T (\lambda (t0: T).(ty3 g c0
 211 (lift (S n) O u) t0)) (lift (S n) O t) (ty3_lift g d u t H1 c0 O (S n)
 212 (getl_drop Abst c0 d u n H0))))))))))) (\lambda (c0: C).(\lambda (u:
 213 T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: (ex T (\lambda
 214 (t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3:
 215 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (_: (ex T
 216 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(\lambda (t4:
 217 T).(\lambda (H4: (ty3 g (CHead c0 (Bind b) u) t3 t4)).(\lambda (H5: (ex T
 218 (\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t4 t5)))).(let H6 \def H5 in
 219 (ex_ind T (\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t4 t5)) (ex T
 220 (\lambda (t5: T).(ty3 g c0 (THead (Bind b) u t3) t5))) (\lambda (x:
 221 T).(\lambda (H7: (ty3 g (CHead c0 (Bind b) u) t4 x)).(ex_intro T (\lambda
 222 (t5: T).(ty3 g c0 (THead (Bind b) u t3) t5)) (THead (Bind b) u t4) (ty3_bind
 223 g c0 u t H0 b t3 t4 H4 x H7)))) H6))))))))))))))) (\lambda (c0: C).(\lambda
 224 (w: T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T
 225 (\lambda (t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda
 226 (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0:
 227 T).(ty3 g c0 (THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T
 228 (\lambda (t0: T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead
 229 (Flat Appl) w (THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_:
 230 (ty3 g c0 u x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0
 231 (THead (Bind Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat
 232 Appl) w (THead (Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g
 233 c0 (THead (Bind Abst) u t) x0)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda
 234 (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst) u t3) x0)))) (\lambda (_:
 235 T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t3:
 236 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t t3))))
 237 (\lambda (t3: T).(\lambda (_: T).(\lambda (t4: T).(ty3 g (CHead c0 (Bind
 238 Abst) u) t3 t4)))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w
 239 (THead (Bind Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda
 240 (x3: T).(\lambda (_: (pc3 c0 (THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3
 241 g c0 u x2)).(\lambda (H10: (ty3 g (CHead c0 (Bind Abst) u) t x1)).(\lambda
 242 (H11: (ty3 g (CHead c0 (Bind Abst) u) x1 x3)).(ex_intro T (\lambda (t0:
 243 T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat
 244 Appl) w (THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u
 245 t) x1 (ty3_bind g c0 u x2 H9 Abst t x1 H10 x3 H11)))))))))) (ty3_gen_bind g
 246 Abst c0 u t x0 H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0:
 247 T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (H1: (ex T
 248 (\lambda (t: T).(ty3 g c0 t3 t)))).(\lambda (t4: T).(\lambda (_: (ty3 g c0 t3
 249 t4)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).H1)))))))) c t1 t2
 250 H))))).
 251
 252 theorem ty3_unique:
 253  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
 254 t1) \to (\forall (t2: T).((ty3 g c u t2) \to (pc3 c t1 t2)))))))
 255 \def
 256  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H:
 257 (ty3 g c u t1)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
 258 T).(\forall (t2: T).((ty3 g c0 t t2) \to (pc3 c0 t0 t2)))))) (\lambda (c0:
 259 C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda
 260 (_: ((\forall (t3: T).((ty3 g c0 t2 t3) \to (pc3 c0 t t3))))).(\lambda (u0:
 261 T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H3: ((\forall
 262 (t3: T).((ty3 g c0 u0 t3) \to (pc3 c0 t0 t3))))).(\lambda (H4: (pc3 c0 t0
 263 t2)).(\lambda (t3: T).(\lambda (H5: (ty3 g c0 u0 t3)).(pc3_t t0 c0 t2 (pc3_s
 264 c0 t2 t0 H4) t3 (H3 t3 H5)))))))))))))) (\lambda (c0: C).(\lambda (m:
 265 nat).(\lambda (t2: T).(\lambda (H0: (ty3 g c0 (TSort m) t2)).(ty3_gen_sort g
 266 c0 t2 m H0))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda
 267 (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr) u0))).(\lambda (t:
 268 T).(\lambda (_: (ty3 g d u0 t)).(\lambda (H2: ((\forall (t2: T).((ty3 g d u0
 269 t2) \to (pc3 d t t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n)
 270 t2)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
 271 T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
 272 (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1:
 273 T).(\lambda (t0: T).(ty3 g e u1 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
 274 (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e:
 275 C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u1)))))
 276 (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))) (pc3 c0
 277 (lift (S n) O t) t2) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_:
 278 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
 279 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
 280 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T
 281 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
 282 t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e
 283 (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g
 284 e u1 t0)))) (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1:
 285 T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x2) t2)).(\lambda
 286 (H6: (getl n c0 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g x0 x1
 287 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n
 288 c0 c1)) H0 (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n
 289 H0 (CHead x0 (Bind Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e:
 290 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d |
 291 (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind
 292 Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr)
 293 x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return
 294 (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t0)
 295 \Rightarrow t0])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1)
 296 (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
 297 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
 298 T).(getl n c0 (CHead x0 (Bind Abbr) t0))) H8 u0 H10) in (let H13 \def
 299 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
 300 (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind Abbr) u0))) H12 d
 301 H11) in (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3 g c1 u0 x2)) H13 d
 302 H11) in (pc3_t (lift (S n) O x2) c0 (lift (S n) O t) (pc3_lift c0 d (S n) O
 303 (getl_drop Abbr c0 d u0 n H14) t x2 (H2 x2 H15)) t2 H5))))))) H9)))))))))
 304 H4)) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
 305 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
 306 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
 307 T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_:
 308 C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda
 309 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst)
 310 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))
 311 (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
 312 T).(\lambda (_: (pc3 c0 (lift (S n) O x1) t2)).(\lambda (H6: (getl n c0
 313 (CHead x0 (Bind Abst) x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def
 314 (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead
 315 x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0
 316 (Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abbr) u0)
 317 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 318 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 319 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
 320 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
 321 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind Abst)
 322 x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abst) x1)
 323 H6)) in (False_ind (pc3 c0 (lift (S n) O t) t2) H9))))))))) H4))
 324 (ty3_gen_lref g c0 t2 n H3)))))))))))) (\lambda (n: nat).(\lambda (c0:
 325 C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind
 326 Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_:
 327 ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t t2))))).(\lambda (t2:
 328 T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(or_ind (ex3_3 C T T (\lambda (_:
 329 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
 330 (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
 331 u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))
 332 (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift
 333 (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
 334 c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
 335 (t0: T).(ty3 g e u1 t0))))) (pc3 c0 (lift (S n) O u0) t2) (\lambda (H4:
 336 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift
 337 (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n
 338 c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda
 339 (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
 340 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda
 341 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e:
 342 C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O
 343 u0) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3
 344 c0 (lift (S n) O x2) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abbr)
 345 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind
 346 Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abbr) x1)
 347 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in
 348 (let H9 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (ee: C).(match ee in
 349 C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k
 350 _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
 351 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
 352 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
 353 \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d
 354 (Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in (False_ind (pc3 c0
 355 (lift (S n) O u0) t2) H9))))))))) H4)) (\lambda (H4: (ex3_3 C T T (\lambda
 356 (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2))))
 357 (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 358 Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1
 359 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_:
 360 T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda
 361 (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1:
 362 T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O u0) t2) (\lambda
 363 (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O
 364 x1) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abst) x1))).(\lambda (H7:
 365 (ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda
 366 (c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d
 367 (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (f_equal
 368 C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 369 \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abst) u0)
 370 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead
 371 x0 (Bind Abst) x1) H6)) in ((let H10 \def (f_equal C T (\lambda (e: C).(match
 372 e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _
 373 t0) \Rightarrow t0])) (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1)
 374 (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in
 375 (\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0:
 376 T).(getl n c0 (CHead x0 (Bind Abst) t0))) H8 u0 H10) in (let H13 \def
 377 (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def
 378 (eq_ind_r T x1 (\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)) H5 u0 H10) in
 379 (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind
 380 Abst) u0))) H12 d H11) in (let H16 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3
 381 g c1 u0 x2)) H13 d H11) in H14))))))) H9))))))))) H4)) (ty3_gen_lref g c0 t2
 382 n H3)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t: T).(\lambda
 383 (_: (ty3 g c0 u0 t)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 u0 t2) \to
 384 (pc3 c0 t t2))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t2: T).(\lambda
 385 (_: (ty3 g (CHead c0 (Bind b) u0) t0 t2)).(\lambda (H3: ((\forall (t3:
 386 T).((ty3 g (CHead c0 (Bind b) u0) t0 t3) \to (pc3 (CHead c0 (Bind b) u0) t2
 387 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t2
 388 t3)).(\lambda (_: ((\forall (t4: T).((ty3 g (CHead c0 (Bind b) u0) t2 t4) \to
 389 (pc3 (CHead c0 (Bind b) u0) t3 t4))))).(\lambda (t4: T).(\lambda (H6: (ty3 g
 390 c0 (THead (Bind b) u0 t0) t4)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_:
 391 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u0 t5) t4)))) (\lambda (_:
 392 T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c0 u0 t6)))) (\lambda (t5:
 393 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u0) t0 t5))))
 394 (\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c0 (Bind b)
 395 u0) t5 t7)))) (pc3 c0 (THead (Bind b) u0 t2) t4) (\lambda (x0: T).(\lambda
 396 (x1: T).(\lambda (x2: T).(\lambda (H7: (pc3 c0 (THead (Bind b) u0 x0)
 397 t4)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H9: (ty3 g (CHead c0 (Bind b)
 398 u0) t0 x0)).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) x0 x2)).(pc3_t (THead
 399 (Bind b) u0 x0) c0 (THead (Bind b) u0 t2) (pc3_head_2 c0 u0 t2 x0 (Bind b)
 400 (H3 x0 H9)) t4 H7)))))))) (ty3_gen_bind g b c0 u0 t0 t4 H6)))))))))))))))))
 401 (\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w
 402 u0)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 w t2) \to (pc3 c0 u0
 403 t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind
 404 Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0
 405 (THead (Bind Abst) u0 t) t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0
 406 (THead (Flat Appl) w v) t2)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t0:
 407 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u1 t0)) t2))) (\lambda
 408 (u1: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u1 t0)))) (\lambda
 409 (u1: T).(\lambda (_: T).(ty3 g c0 w u1))) (pc3 c0 (THead (Flat Appl) w (THead
 410 (Bind Abst) u0 t)) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3
 411 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g
 412 c0 v (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(pc3_t (THead
 413 (Flat Appl) w (THead (Bind Abst) x0 x1)) c0 (THead (Flat Appl) w (THead (Bind
 414 Abst) u0 t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0
 415 x1) (H3 (THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0
 416 w v t2 H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2:
 417 T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0
 418 t0 t3) \to (pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2
 419 t3)).(\lambda (_: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3
 420 t4))))).(\lambda (t4: T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0)
 421 t4)).(and_ind (pc3 c0 t2 t4) (ty3 g c0 t0 t2) (pc3 c0 t2 t4) (\lambda (H5:
 422 (pc3 c0 t2 t4)).(\lambda (_: (ty3 g c0 t0 t2)).H5)) (ty3_gen_cast g c0 t0 t2
 423 t4 H4)))))))))))) c u t1 H))))).
 424
 425 theorem ty3_gen_abst_abst:
 426  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall
 427 (t2: T).((ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (ex2
 428 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst)
 429 u) t1 t2))))))))
 430 \def
 431  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda
 432 (t2: T).(\lambda (H: (ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u
 433 t2))).(ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) u t2) t)) (ex2 T
 434 (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u)
 435 t1 t2))) (\lambda (x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2)
 436 x)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c
 437 (THead (Bind Abst) u t3) x)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_:
 438 T).(ty3 g c u t)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
 439 (CHead c (Bind Abst) u) t2 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda
 440 (t0: T).(ty3 g (CHead c (Bind Abst) u) t3 t0)))) (ex2 T (\lambda (w: T).(ty3
 441 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2))) (\lambda
 442 (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c (THead (Bind
 443 Abst) u x0) x)).(\lambda (_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c
 444 (Bind Abst) u) t2 x0)).(\lambda (_: (ty3 g (CHead c (Bind Abst) u) x0
 445 x2)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c
 446 (THead (Bind Abst) u t3) (THead (Bind Abst) u t2))))) (\lambda (_:
 447 T).(\lambda (t: T).(\lambda (_: T).(ty3 g c u t)))) (\lambda (t3: T).(\lambda
 448 (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t3)))) (\lambda (t3:
 449 T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) t3 t0))))
 450 (ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind
 451 Abst) u) t1 t2))) (\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
 452 (H5: (pc3 c (THead (Bind Abst) u x3) (THead (Bind Abst) u t2))).(\lambda (H6:
 453 (ty3 g c u x4)).(\lambda (H7: (ty3 g (CHead c (Bind Abst) u) t1 x3)).(\lambda
 454 (_: (ty3 g (CHead c (Bind Abst) u) x3 x5)).(and_ind (pc3 c u u) (\forall (b:
 455 B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x3 t2))) (ex2 T (\lambda (w:
 456 T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)))
 457 (\lambda (_: (pc3 c u u)).(\lambda (H10: ((\forall (b: B).(\forall (u0:
 458 T).(pc3 (CHead c (Bind b) u0) x3 t2))))).(ex_intro2 T (\lambda (w: T).(ty3 g
 459 c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x4 H6
 460 (ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x3 H7 (H10 Abst u)))))
 461 (pc3_gen_abst c u u x3 t2 H5))))))))) (ty3_gen_bind g Abst c u t1 (THead
 462 (Bind Abst) u t2) H))))))))) (ty3_gen_bind g Abst c u t2 x H0))))
 463 (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2) H))))))).
 464
 465 theorem ty3_typecheck:
 466  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t
 467 v) \to (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)))))))
 468 \def
 469  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (v: T).(\lambda (H:
 470 (ty3 g c t v)).(ex_ind T (\lambda (t0: T).(ty3 g c v t0)) (ex T (\lambda (u:
 471 T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g
 472 c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)) v
 473 (ty3_cast g c t v H x H0)))) (ty3_correct g c t v H)))))).
 474