matita/matita/contribs/lambdadelta/basic_1A/nf2/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 include "basic_1A/nf2/defs.ma".
  18
  19 include "basic_1A/pr2/fwd.ma".
  20
  21 lemma nf2_sort:
  22  \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
  23 \def
  24  \lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort
  25 n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal
  26 T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
  27
  28 lemma nf2_csort_lref:
  29  \forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
  30 \def
  31  \lambda (n: nat).(\lambda (i: nat).(\lambda (t2: T).(\lambda (H: (pr2 (CSort
  32 n) (TLRef i) t2)).(let H0 \def (pr2_gen_lref (CSort n) t2 i H) in (or_ind (eq
  33 T t2 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort n)
  34 (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S
  35 i) O u))))) (eq T (TLRef i) t2) (\lambda (H1: (eq T t2 (TLRef i))).(eq_ind_r
  36 T (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
  37 H1)) (\lambda (H1: (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
  38 n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
  39 (S i) O u)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
  40 n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
  41 (S i) O u)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
  42 (H2: (getl i (CSort n) (CHead x0 (Bind Abbr) x1))).(\lambda (H3: (eq T t2
  43 (lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T
  44 (TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i)
  45 (lift (S i) O x1))) t2 H3))))) H1)) H0))))).
  46
  47 theorem nf2_abst:
  48  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v:
  49 T).(\forall (t: T).((nf2 (CHead c (Bind b) v) t) \to (nf2 c (THead (Bind
  50 Abst) u t))))))))
  51 \def
  52  \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
  53 \to (eq T u t2))))).(\lambda (b: B).(\lambda (v: T).(\lambda (t: T).(\lambda
  54 (H0: ((\forall (t2: T).((pr2 (CHead c (Bind b) v) t t2) \to (eq T t
  55 t2))))).(\lambda (t2: T).(\lambda (H1: (pr2 c (THead (Bind Abst) u t)
  56 t2)).(let H2 \def (pr2_gen_abst c u t t2 H1) in (ex3_2_ind T T (\lambda (u2:
  57 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
  58 T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
  59 (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t t3))))) (eq T (THead
  60 (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t2
  61 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2 c u x0)).(\lambda (H5:
  62 ((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t
  63 x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
  64 (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t
  65 x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3))))))
  66 H2)))))))))).
  67
  68 theorem nf2_abst_shift:
  69  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c
  70 (Bind Abst) u) t) \to (nf2 c (THead (Bind Abst) u t))))))
  71 \def
  72  \lambda (c: C).(\lambda (u: T).(\lambda (H: ((\forall (t2: T).((pr2 c u t2)
  73 \to (eq T u t2))))).(\lambda (t: T).(\lambda (H0: ((\forall (t2: T).((pr2
  74 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))))).(\lambda (t2: T).(\lambda
  75 (H1: (pr2 c (THead (Bind Abst) u t) t2)).(let H2 \def (pr2_gen_abst c u t t2
  76 H1) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
  77 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_:
  78 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
  79 u0) t t3))))) (eq T (THead (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda
  80 (x1: T).(\lambda (H3: (eq T t2 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2
  81 c u x0)).(\lambda (H5: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
  82 b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
  83 (THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst)
  84 u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
  85 H3)))))) H2)))))))).
  86
  87 lemma nfs2_tapp:
  88  \forall (c: C).(\forall (t: T).(\forall (ts: TList).((nfs2 c (TApp ts t))
  89 \to (land (nfs2 c ts) (nf2 c t)))))
  90 \def
  91  \lambda (c: C).(\lambda (t: T).(\lambda (ts: TList).(TList_ind (\lambda (t0:
  92 TList).((nfs2 c (TApp t0 t)) \to (land (nfs2 c t0) (nf2 c t)))) (\lambda (H:
  93 (land (nf2 c t) True)).(let H0 \def H in (land_ind (nf2 c t) True (land True
  94 (nf2 c t)) (\lambda (H1: (nf2 c t)).(\lambda (_: True).(conj True (nf2 c t) I
  95 H1))) H0))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (((nfs2 c
  96 (TApp t1 t)) \to (land (nfs2 c t1) (nf2 c t))))).(\lambda (H0: (land (nf2 c
  97 t0) (nfs2 c (TApp t1 t)))).(let H1 \def H0 in (land_ind (nf2 c t0) (nfs2 c
  98 (TApp t1 t)) (land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)) (\lambda (H2:
  99 (nf2 c t0)).(\lambda (H3: (nfs2 c (TApp t1 t))).(let H_x \def (H H3) in (let
 100 H4 \def H_x in (land_ind (nfs2 c t1) (nf2 c t) (land (land (nf2 c t0) (nfs2 c
 101 t1)) (nf2 c t)) (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(conj
 102 (land (nf2 c t0) (nfs2 c t1)) (nf2 c t) (conj (nf2 c t0) (nfs2 c t1) H2 H5)
 103 H6))) H4))))) H1)))))) ts))).
 104
 105 lemma nf2_appls_lref:
 106  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs:
 107 TList).((nfs2 c vs) \to (nf2 c (THeads (Flat Appl) vs (TLRef i)))))))
 108 \def
 109  \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
 110 (vs: TList).(TList_ind (\lambda (t: TList).((nfs2 c t) \to (nf2 c (THeads
 111 (Flat Appl) t (TLRef i))))) (\lambda (_: True).H) (\lambda (t: T).(\lambda
 112 (t0: TList).(\lambda (H0: (((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0
 113 (TLRef i)))))).(\lambda (H1: (land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in
 114 (land_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat
 115 Appl) t0 (TLRef i)))) (\lambda (H3: (nf2 c t)).(\lambda (H4: (nfs2 c
 116 t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c (THead
 117 (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let H6 \def
 118 (pr2_gen_appl c t (THeads (Flat Appl) t0 (TLRef i)) t2 H5) in (or3_ind (ex3_2
 119 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
 120 (\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3:
 121 T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t3)))) (ex4_4 T T T T (\lambda
 122 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat
 123 Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
 124 (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
 125 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
 126 T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
 127 (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1
 128 t3)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
 129 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
 130 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
 131 (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind
 132 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
 133 (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead
 134 (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_:
 135 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t
 136 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
 137 T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
 138 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
 139 (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (eq T (THead (Flat Appl) t
 140 (THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (H7: (ex3_2 T T (\lambda (u2:
 141 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
 142 T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
 143 (THeads (Flat Appl) t0 (TLRef i)) t3))))).(ex3_2_ind T T (\lambda (u2:
 144 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
 145 T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
 146 (THeads (Flat Appl) t0 (TLRef i)) t3))) (eq T (THead (Flat Appl) t (THeads
 147 (Flat Appl) t0 (TLRef i))) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda
 148 (H8: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H9: (pr2 c t
 149 x0)).(\lambda (H10: (pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1)).(eq_ind_r T
 150 (THead (Flat Appl) x0 x1) (\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads
 151 (Flat Appl) t0 (TLRef i))) t1)) (let H11 \def (eq_ind_r T x1 (\lambda (t1:
 152 T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t1)) H10 (THeads (Flat Appl) t0
 153 (TLRef i)) (H_y x1 H10)) in (eq_ind T (THeads (Flat Appl) t0 (TLRef i))
 154 (\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef
 155 i))) (THead (Flat Appl) x0 t1))) (let H12 \def (eq_ind_r T x0 (\lambda (t1:
 156 T).(pr2 c t t1)) H9 t (H3 x0 H9)) in (eq_ind T t (\lambda (t1: T).(eq T
 157 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) (THead (Flat Appl) t1
 158 (THeads (Flat Appl) t0 (TLRef i))))) (refl_equal T (THead (Flat Appl) t
 159 (THeads (Flat Appl) t0 (TLRef i)))) x0 (H3 x0 H9))) x1 (H_y x1 H10))) t2
 160 H8)))))) H7)) (\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
 161 T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
 162 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
 163 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
 164 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))) (\lambda
 165 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
 166 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T T T
 167 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
 168 (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
 169 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
 170 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
 171 (_: T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
 172 T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
 173 z1 t3))))))) (eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
 174 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
 175 T).(\lambda (H8: (eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst)
 176 x0 x1))).(\lambda (H9: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2
 177 c t x2)).(\lambda (_: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b)
 178 u) x1 x3))))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t1: T).(eq T
 179 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind
 180 (\lambda (t1: TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T
 181 (THeads (Flat Appl) t1 (TLRef i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead
 182 (Flat Appl) t (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind Abbr) x2
 183 x3))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil (TLRef i)))).(\lambda
 184 (H13: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind Abst) x0
 185 x1))).(let H14 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with
 186 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
 187 \Rightarrow False])) I (THead (Bind Abst) x0 x1) H13) in (False_ind (eq T
 188 (THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind Abbr)
 189 x2 x3)) H14)))) (\lambda (t1: T).(\lambda (t3: TList).(\lambda (_: (((nf2 c
 190 (THeads (Flat Appl) t3 (TLRef i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef
 191 i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead (Flat Appl) t (THeads (Flat
 192 Appl) t3 (TLRef i))) (THead (Bind Abbr) x2 x3)))))).(\lambda (_: (nf2 c
 193 (THeads (Flat Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H13: (eq T (THeads
 194 (Flat Appl) (TCons t1 t3) (TLRef i)) (THead (Bind Abst) x0 x1))).(let H14
 195 \def (eq_ind T (THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)))
 196 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
 197 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
 198 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x0
 199 x1) H13) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat Appl) (TCons
 200 t1 t3) (TLRef i))) (THead (Bind Abbr) x2 x3)) H14))))))) t0 H_y H8) t2
 201 H9))))))))) H7)) (\lambda (H7: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
 202 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
 203 (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
 204 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl)
 205 t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
 206 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
 207 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
 208 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
 209 T).(\lambda (_: T).(pr2 c t u2))))))) (\lambda (_: B).(\lambda (y1:
 210 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
 211 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
 212 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
 213 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
 214 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
 215 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
 216 T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
 217 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
 218 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
 219 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
 220 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
 221 (_: T).(pr2 c t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
 222 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
 223 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
 224 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (eq T (THead
 225 (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (x0:
 226 B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
 227 T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H9: (eq T
 228 (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2))).(\lambda (H10:
 229 (eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
 230 x3)))).(\lambda (_: (pr2 c t x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_:
 231 (pr2 (CHead c (Bind x0) x5) x2 x3)).(eq_ind_r T (THead (Bind x0) x5 (THead
 232 (Flat Appl) (lift (S O) O x4) x3)) (\lambda (t1: T).(eq T (THead (Flat Appl)
 233 t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind (\lambda (t1:
 234 TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat
 235 Appl) t1 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t
 236 (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl)
 237 (lift (S O) O x4) x3)))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil
 238 (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead
 239 (Bind x0) x1 x2))).(let H16 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match
 240 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _
 241 _ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T
 242 (THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind x0) x5
 243 (THead (Flat Appl) (lift (S O) O x4) x3))) H16)))) (\lambda (t1: T).(\lambda
 244 (t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef i))) \to ((eq
 245 T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead
 246 (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead (Bind x0) x5 (THead
 247 (Flat Appl) (lift (S O) O x4) x3))))))).(\lambda (_: (nf2 c (THeads (Flat
 248 Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl)
 249 (TCons t1 t3) (TLRef i)) (THead (Bind x0) x1 x2))).(let H16 \def (eq_ind T
 250 (THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))) (\lambda (ee:
 251 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 252 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat
 253 _) \Rightarrow True])])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T
 254 (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead
 255 (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9)
 256 t2 H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
 257
 258 theorem nf2_appl_lref:
 259  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c
 260 (TLRef i)) \to (nf2 c (THead (Flat Appl) u (TLRef i)))))))
 261 \def
 262  \lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i:
 263 nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0
 264 (TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
 265
 266 lemma nf2_lref_abst:
 267  \forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c
 268 (CHead e (Bind Abst) u)) \to (nf2 c (TLRef i))))))
 269 \def
 270  \lambda (c: C).(\lambda (e: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
 271 (H: (getl i c (CHead e (Bind Abst) u))).(\lambda (t2: T).(\lambda (H0: (pr2 c
 272 (TLRef i) t2)).(let H1 \def (pr2_gen_lref c t2 i H0) in (or_ind (eq T t2
 273 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c (CHead d
 274 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift (S i) O
 275 u0))))) (eq T (TLRef i) t2) (\lambda (H2: (eq T t2 (TLRef i))).(eq_ind_r T
 276 (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
 277 H2)) (\lambda (H2: (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c
 278 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
 279 (S i) O u0)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u0: T).(getl i c
 280 (CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
 281 (S i) O u0)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
 282 (H3: (getl i c (CHead x0 (Bind Abbr) x1))).(\lambda (H4: (eq T t2 (lift (S i)
 283 O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T (TLRef i) t))
 284 (let H5 \def (eq_ind C (CHead e (Bind Abst) u) (\lambda (c0: C).(getl i c
 285 c0)) H (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H
 286 (CHead x0 (Bind Abbr) x1) H3)) in (let H6 \def (eq_ind C (CHead e (Bind Abst)
 287 u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k
 288 _) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
 289 \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
 290 _) \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e
 291 (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1) H3)) in (False_ind (eq T (TLRef
 292 i) (lift (S i) O x1)) H6))) t2 H4))))) H2)) H1)))))))).
 293
 294 lemma nf2_lift:
 295  \forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h:
 296 nat).(\forall (i: nat).((drop h i c d) \to (nf2 c (lift h i t))))))))
 297 \def
 298  \lambda (d: C).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).((pr2 d t t2)
 299 \to (eq T t t2))))).(\lambda (c: C).(\lambda (h: nat).(\lambda (i:
 300 nat).(\lambda (H0: (drop h i c d)).(\lambda (t2: T).(\lambda (H1: (pr2 c
 301 (lift h i t) t2)).(let H2 \def (pr2_gen_lift c t t2 h i H1 d H0) in (ex2_ind
 302 T (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t t3))
 303 (eq T (lift h i t) t2) (\lambda (x: T).(\lambda (H3: (eq T t2 (lift h i
 304 x))).(\lambda (H4: (pr2 d t x)).(eq_ind_r T (lift h i x) (\lambda (t0: T).(eq
 305 T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
 306 (\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq
 307 T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3))))
 308 H2)))))))))).
 309