matita/matita/contribs/lambdadelta/basic_1A/pc3/fwd.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1A/pc3/props.ma".
  18
  19 lemma pc3_gen_sort:
  20  \forall (c: C).(\forall (m: nat).(\forall (n: nat).((pc3 c (TSort m) (TSort
  21 n)) \to (eq nat m n))))
  22 \def
  23  \lambda (c: C).(\lambda (m: nat).(\lambda (n: nat).(\lambda (H: (pc3 c
  24 (TSort m) (TSort n))).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c
  25 (TSort m) t)) (\lambda (t: T).(pr3 c (TSort n) t)) (eq nat m n) (\lambda (x:
  26 T).(\lambda (H1: (pr3 c (TSort m) x)).(\lambda (H2: (pr3 c (TSort n) x)).(let
  27 H3 \def (eq_ind T x (\lambda (t: T).(eq T t (TSort n))) (pr3_gen_sort c x n
  28 H2) (TSort m) (pr3_gen_sort c x m H1)) in (let H4 \def (f_equal T nat
  29 (\lambda (e: T).(match e with [(TSort n0) \Rightarrow n0 | (TLRef _)
  30 \Rightarrow m | (THead _ _ _) \Rightarrow m])) (TSort m) (TSort n) H3) in
  31 H4))))) H0))))).
  32
  33 lemma pc3_gen_abst:
  34  \forall (c: C).(\forall (u1: T).(\forall (u2: T).(\forall (t1: T).(\forall
  35 (t2: T).((pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)) \to
  36 (land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)
  37 t1 t2)))))))))
  38 \def
  39  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (t1: T).(\lambda
  40 (t2: T).(\lambda (H: (pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2
  41 t2))).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c (THead (Bind Abst)
  42 u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 t2) t)) (land (pc3 c
  43 u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2))))
  44 (\lambda (x: T).(\lambda (H1: (pr3 c (THead (Bind Abst) u1 t1) x)).(\lambda
  45 (H2: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H3 \def (pr3_gen_abst c u2 t2
  46 x H2) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
  47 (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3)))
  48 (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
  49 c (Bind b) u) t2 t3))))) (land (pc3 c u1 u2) (\forall (b: B).(\forall (u:
  50 T).(pc3 (CHead c (Bind b) u) t1 t2)))) (\lambda (x0: T).(\lambda (x1:
  51 T).(\lambda (H4: (eq T x (THead (Bind Abst) x0 x1))).(\lambda (H5: (pr3 c u2
  52 x0)).(\lambda (H6: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
  53 t2 x1))))).(let H7 \def (pr3_gen_abst c u1 t1 x H1) in (ex3_2_ind T T
  54 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
  55 (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda
  56 (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t3)))))
  57 (land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)
  58 t1 t2)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T x (THead
  59 (Bind Abst) x2 x3))).(\lambda (H9: (pr3 c u1 x2)).(\lambda (H10: ((\forall
  60 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 x3))))).(let H11 \def
  61 (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Abst) x0 x1))) H4 (THead
  62 (Bind Abst) x2 x3) H8) in (let H12 \def (f_equal T T (\lambda (e: T).(match e
  63 with [(TSort _) \Rightarrow x2 | (TLRef _) \Rightarrow x2 | (THead _ t _)
  64 \Rightarrow t])) (THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1) H11) in
  65 ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
  66 \Rightarrow x3 | (TLRef _) \Rightarrow x3 | (THead _ _ t) \Rightarrow t]))
  67 (THead (Bind Abst) x2 x3) (THead (Bind Abst) x0 x1) H11) in (\lambda (H14:
  68 (eq T x2 x0)).(let H15 \def (eq_ind T x3 (\lambda (t: T).(\forall (b:
  69 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t)))) H10 x1 H13) in (let H16
  70 \def (eq_ind T x2 (\lambda (t: T).(pr3 c u1 t)) H9 x0 H14) in (conj (pc3 c u1
  71 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u) t1 t2)))
  72 (pc3_pr3_t c u1 x0 H16 u2 H5) (\lambda (b: B).(\lambda (u: T).(pc3_pr3_t
  73 (CHead c (Bind b) u) t1 x1 (H15 b u) t2 (H6 b u))))))))) H12))))))))
  74 H7))))))) H3))))) H0))))))).
  75
  76 lemma pc3_gen_abst_shift:
  77  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).((pc3 c
  78 (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (pc3 (CHead c (Bind
  79 Abst) u) t1 t2)))))
  80 \def
  81  \lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  82 (H: (pc3 c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2))).(let H_x \def
  83 (pc3_gen_abst c u u t1 t2 H) in (let H0 \def H_x in (land_ind (pc3 c u u)
  84 (\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))) (pc3
  85 (CHead c (Bind Abst) u) t1 t2) (\lambda (_: (pc3 c u u)).(\lambda (H2:
  86 ((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))))).(H2
  87 Abst u))) H0))))))).
  88
  89 lemma pc3_gen_lift:
  90  \forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (h: nat).(\forall
  91 (d: nat).((pc3 c (lift h d t1) (lift h d t2)) \to (\forall (e: C).((drop h d
  92 c e) \to (pc3 e t1 t2))))))))
  93 \def
  94  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (h: nat).(\lambda
  95 (d: nat).(\lambda (H: (pc3 c (lift h d t1) (lift h d t2))).(\lambda (e:
  96 C).(\lambda (H0: (drop h d c e)).(let H1 \def H in (ex2_ind T (\lambda (t:
  97 T).(pr3 c (lift h d t1) t)) (\lambda (t: T).(pr3 c (lift h d t2) t)) (pc3 e
  98 t1 t2) (\lambda (x: T).(\lambda (H2: (pr3 c (lift h d t1) x)).(\lambda (H3:
  99 (pr3 c (lift h d t2) x)).(let H4 \def (pr3_gen_lift c t2 x h d H3 e H0) in
 100 (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3: T).(pr3 e
 101 t2 t3)) (pc3 e t1 t2) (\lambda (x0: T).(\lambda (H5: (eq T x (lift h d
 102 x0))).(\lambda (H6: (pr3 e t2 x0)).(let H7 \def (pr3_gen_lift c t1 x h d H2 e
 103 H0) in (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3:
 104 T).(pr3 e t1 t3)) (pc3 e t1 t2) (\lambda (x1: T).(\lambda (H8: (eq T x (lift
 105 h d x1))).(\lambda (H9: (pr3 e t1 x1)).(let H10 \def (eq_ind T x (\lambda (t:
 106 T).(eq T t (lift h d x0))) H5 (lift h d x1) H8) in (let H11 \def (eq_ind T x1
 107 (\lambda (t: T).(pr3 e t1 t)) H9 x0 (lift_inj x1 x0 h d H10)) in (pc3_pr3_t e
 108 t1 x0 H11 t2 H6)))))) H7))))) H4))))) H1))))))))).
 109
 110 lemma pc3_gen_not_abst:
 111  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (t1:
 112 T).(\forall (t2: T).(\forall (u1: T).(\forall (u2: T).((pc3 c (THead (Bind b)
 113 u1 t1) (THead (Bind Abst) u2 t2)) \to (pc3 (CHead c (Bind b) u1) t1 (lift (S
 114 O) O (THead (Bind Abst) u2 t2))))))))))
 115 \def
 116  \lambda (b: B).(B_ind (\lambda (b0: B).((not (eq B b0 Abst)) \to (\forall
 117 (c: C).(\forall (t1: T).(\forall (t2: T).(\forall (u1: T).(\forall (u2:
 118 T).((pc3 c (THead (Bind b0) u1 t1) (THead (Bind Abst) u2 t2)) \to (pc3 (CHead
 119 c (Bind b0) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))))))))))) (\lambda
 120 (_: (not (eq B Abbr Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2:
 121 T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Abbr)
 122 u1 t1) (THead (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t:
 123 T).(pr3 c (THead (Bind Abbr) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind
 124 Abst) u2 t2) t)) (pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind
 125 Abst) u2 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Abbr) u1 t1)
 126 x)).(\lambda (H3: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H4 \def
 127 (pr3_gen_abbr c u1 t1 x H2) in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda
 128 (t3: T).(eq T x (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_:
 129 T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr3 (CHead c (Bind Abbr)
 130 u1) t1 t3)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)) (pc3 (CHead
 131 c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (H5:
 132 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abbr) u3
 133 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_:
 134 T).(\lambda (t3: T).(pr3 (CHead c (Bind Abbr) u1) t1 t3))))).(ex3_2_ind T T
 135 (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abbr) u3 t3))))
 136 (\lambda (u3: T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda
 137 (t3: T).(pr3 (CHead c (Bind Abbr) u1) t1 t3))) (pc3 (CHead c (Bind Abbr) u1)
 138 t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0: T).(\lambda (x1:
 139 T).(\lambda (H6: (eq T x (THead (Bind Abbr) x0 x1))).(\lambda (_: (pr3 c u1
 140 x0)).(\lambda (_: (pr3 (CHead c (Bind Abbr) u1) t1 x1)).(let H9 \def
 141 (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3:
 142 T).(eq T x (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3
 143 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u:
 144 T).(pr3 (CHead c (Bind b0) u) t2 t3))))) (pc3 (CHead c (Bind Abbr) u1) t1
 145 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x2: T).(\lambda (x3:
 146 T).(\lambda (H10: (eq T x (THead (Bind Abst) x2 x3))).(\lambda (_: (pr3 c u2
 147 x2)).(\lambda (_: ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0)
 148 u) t2 x3))))).(let H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind
 149 Abbr) x0 x1))) H6 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T
 150 (THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee with [(TSort _)
 151 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 152 (match k with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow False |
 153 Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow
 154 False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3 (CHead c (Bind
 155 Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) H14)))))))) H9)))))))
 156 H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x))).(let
 157 H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3:
 158 T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3)))) (\lambda (u3:
 159 T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall
 160 (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 t3))))) (pc3 (CHead c
 161 (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0:
 162 T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind Abst) x0
 163 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0: B).(\forall
 164 (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def (eq_ind T x
 165 (\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O t))) H5 (THead
 166 (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1) t1 (lift (S O)
 167 O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind Abst) u2 t2))
 168 (pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind Abbr) O c c
 169 (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 x1)
 170 (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6))) H4)))))
 171 H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c: C).(\lambda
 172 (t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pc3
 173 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2))).(let H1 \def (match
 174 (H (refl_equal B Abst)) in False with []) in H1)))))))) (\lambda (_: (not (eq
 175 B Void Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 176 (u1: T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1)
 177 (THead (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t:
 178 T).(pr3 c (THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind
 179 Abst) u2 t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind
 180 Abst) u2 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1)
 181 x)).(\lambda (H3: (pr3 c (THead (Bind Abst) u2 t2) x)).(let H4 \def
 182 (pr3_gen_void c u1 t1 x H2) in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda
 183 (t3: T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_:
 184 T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall
 185 (u: T).(pr3 (CHead c (Bind b0) u) t1 t3)))))) (pr3 (CHead c (Bind Void) u1)
 186 t1 (lift (S O) O x)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead
 187 (Bind Abst) u2 t2))) (\lambda (H5: (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
 188 T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3
 189 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u:
 190 T).(pr3 (CHead c (Bind b0) u) t1 t3))))))).(ex3_2_ind T T (\lambda (u3:
 191 T).(\lambda (t3: T).(eq T x (THead (Bind Void) u3 t3)))) (\lambda (u3:
 192 T).(\lambda (_: T).(pr3 c u1 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall
 193 (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t1 t3))))) (pc3 (CHead c
 194 (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0:
 195 T).(\lambda (x1: T).(\lambda (H6: (eq T x (THead (Bind Void) x0
 196 x1))).(\lambda (_: (pr3 c u1 x0)).(\lambda (_: ((\forall (b0: B).(\forall (u:
 197 T).(pr3 (CHead c (Bind b0) u) t1 x1))))).(let H9 \def (pr3_gen_abst c u2 t2 x
 198 H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind
 199 Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_:
 200 T).(\lambda (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0)
 201 u) t2 t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind
 202 Abst) u2 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H10: (eq T x
 203 (THead (Bind Abst) x2 x3))).(\lambda (_: (pr3 c u2 x2)).(\lambda (_:
 204 ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x3))))).(let
 205 H13 \def (eq_ind T x (\lambda (t: T).(eq T t (THead (Bind Void) x0 x1))) H6
 206 (THead (Bind Abst) x2 x3) H10) in (let H14 \def (eq_ind T (THead (Bind Abst)
 207 x2 x3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef
 208 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind b0)
 209 \Rightarrow (match b0 with [Abbr \Rightarrow False | Abst \Rightarrow True |
 210 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (THead (Bind
 211 Void) x0 x1) H13) in (False_ind (pc3 (CHead c (Bind Void) u1) t1 (lift (S O)
 212 O (THead (Bind Abst) u2 t2))) H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3
 213 (CHead c (Bind Void) u1) t1 (lift (S O) O x))).(let H6 \def (pr3_gen_abst c
 214 u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x
 215 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3)))
 216 (\lambda (_: T).(\lambda (t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead
 217 c (Bind b0) u) t2 t3))))) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O
 218 (THead (Bind Abst) u2 t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7:
 219 (eq T x (THead (Bind Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda
 220 (H9: ((\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2
 221 x1))))).(let H10 \def (eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Void)
 222 u1) t1 (lift (S O) O t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t
 223 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10
 224 (lift (S O) O (THead (Bind Abst) u2 t2)) (pr3_lift (CHead c (Bind Void) u1) c
 225 (S O) O (drop_drop (Bind Void) O c c (drop_refl c) u1) (THead (Bind Abst) u2
 226 t2) (THead (Bind Abst) x0 x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9
 227 Abst x0)))))))))) H6))) H4))))) H1))))))))) b).
 228
 229 lemma pc3_gen_lift_abst:
 230  \forall (c: C).(\forall (t: T).(\forall (t2: T).(\forall (u2: T).(\forall
 231 (h: nat).(\forall (d: nat).((pc3 c (lift h d t) (THead (Bind Abst) u2 t2))
 232 \to (\forall (e: C).((drop h d c e) \to (ex3_2 T T (\lambda (u1: T).(\lambda
 233 (t1: T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_:
 234 T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b:
 235 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d)
 236 t1)))))))))))))))
 237 \def
 238  \lambda (c: C).(\lambda (t: T).(\lambda (t2: T).(\lambda (u2: T).(\lambda
 239 (h: nat).(\lambda (d: nat).(\lambda (H: (pc3 c (lift h d t) (THead (Bind
 240 Abst) u2 t2))).(\lambda (e: C).(\lambda (H0: (drop h d c e)).(let H1 \def H
 241 in (ex2_ind T (\lambda (t0: T).(pr3 c (lift h d t) t0)) (\lambda (t0: T).(pr3
 242 c (THead (Bind Abst) u2 t2) t0)) (ex3_2 T T (\lambda (u1: T).(\lambda (t1:
 243 T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_:
 244 T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b:
 245 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1)))))))
 246 (\lambda (x: T).(\lambda (H2: (pr3 c (lift h d t) x)).(\lambda (H3: (pr3 c
 247 (THead (Bind Abst) u2 t2) x)).(let H4 \def (pr3_gen_lift c t x h d H2 e H0)
 248 in (ex2_ind T (\lambda (t3: T).(eq T x (lift h d t3))) (\lambda (t3: T).(pr3
 249 e t t3)) (ex3_2 T T (\lambda (u1: T).(\lambda (t1: T).(pr3 e t (THead (Bind
 250 Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_: T).(pr3 c u2 (lift h d u1))))
 251 (\lambda (_: T).(\lambda (t1: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
 252 c (Bind b) u) t2 (lift h (S d) t1))))))) (\lambda (x0: T).(\lambda (H5: (eq T
 253 x (lift h d x0))).(\lambda (H6: (pr3 e t x0)).(let H7 \def (pr3_gen_abst c u2
 254 t2 x H3) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
 255 (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3)))
 256 (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
 257 c (Bind b) u) t2 t3))))) (ex3_2 T T (\lambda (u1: T).(\lambda (t1: T).(pr3 e
 258 t (THead (Bind Abst) u1 t1)))) (\lambda (u1: T).(\lambda (_: T).(pr3 c u2
 259 (lift h d u1)))) (\lambda (_: T).(\lambda (t1: T).(\forall (b: B).(\forall
 260 (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))))))) (\lambda (x1:
 261 T).(\lambda (x2: T).(\lambda (H8: (eq T x (THead (Bind Abst) x1
 262 x2))).(\lambda (H9: (pr3 c u2 x1)).(\lambda (H10: ((\forall (b: B).(\forall
 263 (u: T).(pr3 (CHead c (Bind b) u) t2 x2))))).(let H11 \def (eq_ind T x
 264 (\lambda (t0: T).(eq T t0 (lift h d x0))) H5 (THead (Bind Abst) x1 x2) H8) in
 265 (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x0 (THead (Bind Abst) y
 266 z)))) (\lambda (y: T).(\lambda (_: T).(eq T x1 (lift h d y)))) (\lambda (_:
 267 T).(\lambda (z: T).(eq T x2 (lift h (S d) z)))) (ex3_2 T T (\lambda (u1:
 268 T).(\lambda (t1: T).(pr3 e t (THead (Bind Abst) u1 t1)))) (\lambda (u1:
 269 T).(\lambda (_: T).(pr3 c u2 (lift h d u1)))) (\lambda (_: T).(\lambda (t1:
 270 T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 (lift h (S d)
 271 t1))))))) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H12: (eq T x0 (THead
 272 (Bind Abst) x3 x4))).(\lambda (H13: (eq T x1 (lift h d x3))).(\lambda (H14:
 273 (eq T x2 (lift h (S d) x4))).(let H15 \def (eq_ind T x2 (\lambda (t0:
 274 T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t2 t0)))) H10
 275 (lift h (S d) x4) H14) in (let H16 \def (eq_ind T x1 (\lambda (t0: T).(pr3 c
 276 u2 t0)) H9 (lift h d x3) H13) in (let H17 \def (eq_ind T x0 (\lambda (t0:
 277 T).(pr3 e t t0)) H6 (THead (Bind Abst) x3 x4) H12) in (ex3_2_intro T T
 278 (\lambda (u1: T).(\lambda (t1: T).(pr3 e t (THead (Bind Abst) u1 t1))))
 279 (\lambda (u1: T).(\lambda (_: T).(pr3 c u2 (lift h d u1)))) (\lambda (_:
 280 T).(\lambda (t1: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
 281 t2 (lift h (S d) t1)))))) x3 x4 H17 H16 H15))))))))) (lift_gen_bind Abst x1
 282 x2 x0 h d H11)))))))) H7))))) H4))))) H1)))))))))).
 283
 284 lemma pc3_gen_sort_abst:
 285  \forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (n: nat).((pc3 c
 286 (TSort n) (THead (Bind Abst) u t)) \to (\forall (P: Prop).P)))))
 287 \def
 288  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (n: nat).(\lambda
 289 (H: (pc3 c (TSort n) (THead (Bind Abst) u t))).(\lambda (P: Prop).(let H0
 290 \def H in (ex2_ind T (\lambda (t0: T).(pr3 c (TSort n) t0)) (\lambda (t0:
 291 T).(pr3 c (THead (Bind Abst) u t) t0)) P (\lambda (x: T).(\lambda (H1: (pr3 c
 292 (TSort n) x)).(\lambda (H2: (pr3 c (THead (Bind Abst) u t) x)).(let H3 \def
 293 (pr3_gen_abst c u t x H2) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t2:
 294 T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
 295 c u u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u0:
 296 T).(pr3 (CHead c (Bind b) u0) t t2))))) P (\lambda (x0: T).(\lambda (x1:
 297 T).(\lambda (H4: (eq T x (THead (Bind Abst) x0 x1))).(\lambda (_: (pr3 c u
 298 x0)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
 299 u0) t x1))))).(let H7 \def (eq_ind T x (\lambda (t0: T).(eq T t0 (TSort n)))
 300 (pr3_gen_sort c x n H1) (THead (Bind Abst) x0 x1) H4) in (let H8 \def (eq_ind
 301 T (THead (Bind Abst) x0 x1) (\lambda (ee: T).(match ee with [(TSort _)
 302 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
 303 True])) I (TSort n) H7) in (False_ind P H8)))))))) H3))))) H0))))))).
 304