matita/matita/contribs/lambdadelta/basic_1/sty0/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-1/sty0/defs.ma".
  18
  19 theorem sty0_gen_sort:
  20  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c
  21 (TSort n) x) \to (eq T x (TSort (next g n)))))))
  22 \def
  23  \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
  24 (H: (sty0 g c (TSort n) x)).(insert_eq T (TSort n) (\lambda (t: T).(sty0 g c
  25 t x)) (\lambda (_: T).(eq T x (TSort (next g n)))) (\lambda (y: T).(\lambda
  26 (H0: (sty0 g c y x)).(sty0_ind g (\lambda (_: C).(\lambda (t: T).(\lambda
  27 (t0: T).((eq T t (TSort n)) \to (eq T t0 (TSort (next g n))))))) (\lambda (_:
  28 C).(\lambda (n0: nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def
  29 (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with
  30 [(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _)
  31 \Rightarrow n0])) (TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1:
  32 nat).(eq T (TSort (next g n1)) (TSort (next g n)))) (refl_equal T (TSort
  33 (next g n))) n0 H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v:
  34 T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr)
  35 v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v
  36 (TSort n)) \to (eq T w (TSort (next g n)))))).(\lambda (H4: (eq T (TLRef i)
  37 (TSort n))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T
  38 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
  39 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in
  40 (False_ind (eq T (lift (S i) O w) (TSort (next g n))) H5))))))))))) (\lambda
  41 (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl
  42 i c0 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
  43 w)).(\lambda (_: (((eq T v (TSort n)) \to (eq T w (TSort (next g
  44 n)))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T
  45 (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
  46 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
  47 \Rightarrow False])) I (TSort n) H4) in (False_ind (eq T (lift (S i) O v)
  48 (TSort (next g n))) H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda
  49 (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind
  50 b) v) t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g
  51 n)))))).(\lambda (H3: (eq T (THead (Bind b) v t1) (TSort n))).(let H4 \def
  52 (eq_ind T (THead (Bind b) v t1) (\lambda (ee: T).(match ee in T return
  53 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
  54 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in
  55 (False_ind (eq T (THead (Bind b) v t2) (TSort (next g n))) H4))))))))))
  56 (\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  57 (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort
  58 (next g n)))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TSort n))).(let
  59 H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match ee in T
  60 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
  61 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in
  62 (False_ind (eq T (THead (Flat Appl) v t2) (TSort (next g n))) H4)))))))))
  63 (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1
  64 v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2 (TSort (next g
  65 n)))))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1
  66 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g
  67 n)))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t1) (TSort n))).(let H6
  68 \def (eq_ind T (THead (Flat Cast) v1 t1) (\lambda (ee: T).(match ee in T
  69 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
  70 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in
  71 (False_ind (eq T (THead (Flat Cast) v2 t2) (TSort (next g n))) H6))))))))))))
  72 c y x H0))) H))))).
  73 (* COMMENTS
  74 Initial nodes: 869
  75 END *)
  76
  77 theorem sty0_gen_lref:
  78  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c
  79 (TLRef n) x) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
  80 (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
  81 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
  82 (t: T).(eq T x (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
  83 (u: T).(\lambda (_: T).(getl n c (CHead e (Bind Abst) u))))) (\lambda (e:
  84 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
  85 (u: T).(\lambda (_: T).(eq T x (lift (S n) O u)))))))))))
  86 \def
  87  \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
  88 (H: (sty0 g c (TLRef n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(sty0 g c
  89 t x)) (\lambda (_: T).(or (ex3_3 C T T (\lambda (e: C).(\lambda (u:
  90 T).(\lambda (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e:
  91 C).(\lambda (u: T).(\lambda (t0: T).(sty0 g e u t0)))) (\lambda (_:
  92 C).(\lambda (_: T).(\lambda (t0: T).(eq T x (lift (S n) O t0)))))) (ex3_3 C T
  93 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead e (Bind
  94 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(sty0 g e u
  95 t0)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T x (lift (S n) O
  96 u)))))))) (\lambda (y: T).(\lambda (H0: (sty0 g c y x)).(sty0_ind g (\lambda
  97 (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n)) \to (or (ex3_3 C
  98 T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
  99 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t1: T).(sty0 g e u
 100 t1)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t1: T).(eq T t0 (lift (S n)
 101 O t1)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
 102 n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda
 103 (t1: T).(sty0 g e u t1)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_:
 104 T).(eq T t0 (lift (S n) O u))))))))))) (\lambda (c0: C).(\lambda (n0:
 105 nat).(\lambda (H1: (eq T (TSort n0) (TLRef n))).(let H2 \def (eq_ind T (TSort
 106 n0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
 107 _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
 108 False])) I (TLRef n) H1) in (False_ind (or (ex3_3 C T T (\lambda (e:
 109 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
 110 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
 111 (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (TSort (next g n0)) (lift (S n)
 112 O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
 113 n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
 114 T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T
 115 (TSort (next g n0)) (lift (S n) O u))))))) H2))))) (\lambda (c0: C).(\lambda
 116 (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d
 117 (Bind Abbr) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_:
 118 (((eq T v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u:
 119 T).(\lambda (_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e:
 120 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
 121 (_: T).(\lambda (t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda
 122 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u)))))
 123 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
 124 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T w (lift (S n) O
 125 u)))))))))).(\lambda (H4: (eq T (TLRef i) (TLRef n))).(let H5 \def (f_equal T
 126 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
 127 \Rightarrow i | (TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i]))
 128 (TLRef i) (TLRef n) H4) in (let H6 \def (eq_ind nat i (\lambda (n0:
 129 nat).(getl n0 c0 (CHead d (Bind Abbr) v))) H1 n H5) in (eq_ind_r nat n
 130 (\lambda (n0: nat).(or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 131 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 132 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 133 (t: T).(eq T (lift (S n0) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda
 134 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
 135 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
 136 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n0) O w) (lift (S n) O
 137 u)))))))) (or_introl (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 138 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 139 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 140 (t: T).(eq T (lift (S n) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e:
 141 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
 142 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
 143 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n) O w) (lift (S n) O
 144 u)))))) (ex3_3_intro C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
 145 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 146 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 147 (t: T).(eq T (lift (S n) O w) (lift (S n) O t))))) d v w H6 H2 (refl_equal T
 148 (lift (S n) O w)))) i H5)))))))))))) (\lambda (c0: C).(\lambda (d:
 149 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d (Bind
 150 Abst) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: (((eq T
 151 v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 152 (_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 153 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 154 (t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
 155 (u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u))))) (\lambda (e:
 156 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
 157 (u: T).(\lambda (_: T).(eq T w (lift (S n) O u)))))))))).(\lambda (H4: (eq T
 158 (TLRef i) (TLRef n))).(let H5 \def (f_equal T nat (\lambda (e: T).(match e in
 159 T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n0)
 160 \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n) H4) in
 161 (let H6 \def (eq_ind nat i (\lambda (n0: nat).(getl n0 c0 (CHead d (Bind
 162 Abst) v))) H1 n H5) in (eq_ind_r nat n (\lambda (n0: nat).(or (ex3_3 C T T
 163 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 164 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 165 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n0) O v)
 166 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 167 (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
 168 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
 169 (_: T).(eq T (lift (S n0) O v) (lift (S n) O u)))))))) (or_intror (ex3_3 C T
 170 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 171 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 172 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n) O v)
 173 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 174 (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
 175 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
 176 (_: T).(eq T (lift (S n) O v) (lift (S n) O u)))))) (ex3_3_intro C T T
 177 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 178 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 179 t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n) O v)
 180 (lift (S n) O u))))) d v w H6 H2 (refl_equal T (lift (S n) O v)))) i
 181 H5)))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t1:
 182 T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t1
 183 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e:
 184 C).(\lambda (u: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) v) (CHead e
 185 (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e
 186 u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n)
 187 O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
 188 n (CHead c0 (Bind b) v) (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda
 189 (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u:
 190 T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H3: (eq T
 191 (THead (Bind b) v t1) (TLRef n))).(let H4 \def (eq_ind T (THead (Bind b) v
 192 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
 193 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
 194 \Rightarrow True])) I (TLRef n) H3) in (False_ind (or (ex3_3 C T T (\lambda
 195 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
 196 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
 197 (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Bind b) v t2) (lift (S
 198 n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
 199 T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
 200 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
 201 (_: T).(eq T (THead (Bind b) v t2) (lift (S n) O u))))))) H4))))))))))
 202 (\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 203 (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T
 204 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 205 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 206 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n) O
 207 t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n
 208 c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
 209 T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T t2
 210 (lift (S n) O u)))))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TLRef
 211 n))).(let H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match
 212 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
 213 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n)
 214 H3) in (False_ind (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
 215 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 216 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 217 (t: T).(eq T (THead (Flat Appl) v t2) (lift (S n) O t)))))) (ex3_3 C T T
 218 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 219 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 220 t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (THead (Flat
 221 Appl) v t2) (lift (S n) O u))))))) H4))))))))) (\lambda (c0: C).(\lambda (v1:
 222 T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1
 223 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
 224 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 225 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 226 (t: T).(eq T v2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
 227 (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
 228 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
 229 (u: T).(\lambda (_: T).(eq T v2 (lift (S n) O u)))))))))).(\lambda (t1:
 230 T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1
 231 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
 232 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
 233 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
 234 (t: T).(eq T t2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
 235 (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
 236 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
 237 (u: T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H5: (eq T
 238 (THead (Flat Cast) v1 t1) (TLRef n))).(let H6 \def (eq_ind T (THead (Flat
 239 Cast) v1 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
 240 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
 241 _) \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T
 242 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
 243 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
 244 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Flat
 245 Cast) v2 t2) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u:
 246 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
 247 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
 248 (u: T).(\lambda (_: T).(eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)))))))
 249 H6)))))))))))) c y x H0))) H))))).
 250 (* COMMENTS
 251 Initial nodes: 3231
 252 END *)
 253
 254 theorem sty0_gen_bind:
 255  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1:
 256 T).(\forall (x: T).((sty0 g c (THead (Bind b) u t1) x) \to (ex2 T (\lambda
 257 (t2: T).(sty0 g (CHead c (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T x (THead
 258 (Bind b) u t2))))))))))
 259 \def
 260  \lambda (g: G).(\lambda (b: B).(\lambda (c: C).(\lambda (u: T).(\lambda (t1:
 261 T).(\lambda (x: T).(\lambda (H: (sty0 g c (THead (Bind b) u t1)
 262 x)).(insert_eq T (THead (Bind b) u t1) (\lambda (t: T).(sty0 g c t x))
 263 (\lambda (_: T).(ex2 T (\lambda (t2: T).(sty0 g (CHead c (Bind b) u) t1 t2))
 264 (\lambda (t2: T).(eq T x (THead (Bind b) u t2))))) (\lambda (y: T).(\lambda
 265 (H0: (sty0 g c y x)).(sty0_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda
 266 (t0: T).((eq T t (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g
 267 (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T t0 (THead (Bind b) u
 268 t2)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n)
 269 (THead (Bind b) u t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee:
 270 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 271 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
 272 (THead (Bind b) u t1) H1) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g
 273 (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (TSort (next g n))
 274 (THead (Bind b) u t2)))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
 275 (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr)
 276 v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v
 277 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind b)
 278 u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda (H4:
 279 (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i)
 280 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
 281 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
 282 False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2:
 283 T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O
 284 w) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d:
 285 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind
 286 Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T
 287 v (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind
 288 b) u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda
 289 (H4: (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i)
 290 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
 291 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
 292 False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2:
 293 T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O
 294 v) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (b0: B).(\lambda (c0:
 295 C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g
 296 (CHead c0 (Bind b0) v) t0 t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u
 297 t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind
 298 b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
 299 (H3: (eq T (THead (Bind b0) v t0) (THead (Bind b) u t1))).(let H4 \def
 300 (f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with
 301 [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _)
 302 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
 303 \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v t0) (THead
 304 (Bind b) u t1) H3) in ((let H5 \def (f_equal T T (\lambda (e: T).(match e in
 305 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _)
 306 \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v t0) (THead
 307 (Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e: T).(match e in
 308 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
 309 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead
 310 (Bind b) u t1) H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0
 311 b)).(let H9 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1))
 312 \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u)
 313 t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in
 314 (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t
 315 t2)) H1 t1 H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead
 316 (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind
 317 b0) t) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u
 318 t3)))))) H9 u H7) in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead
 319 c0 (Bind b0) t) t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T
 320 (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T
 321 (THead (Bind b0) t t2) (THead (Bind b) u t3))))) (let H13 \def (eq_ind B b0
 322 (\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3:
 323 T).(sty0 g (CHead (CHead c0 (Bind b1) u) (Bind b) u) t1 t3)) (\lambda (t3:
 324 T).(eq T t2 (THead (Bind b) u t3)))))) H11 b H8) in (let H14 \def (eq_ind B
 325 b0 (\lambda (b1: B).(sty0 g (CHead c0 (Bind b1) u) t1 t2)) H12 b H8) in
 326 (eq_ind_r B b (\lambda (b1: B).(ex2 T (\lambda (t3: T).(sty0 g (CHead c0
 327 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b1) u t2) (THead
 328 (Bind b) u t3))))) (ex_intro2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
 329 u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) u t2) (THead (Bind b) u
 330 t3))) t2 H14 (refl_equal T (THead (Bind b) u t2))) b0 H8))) v H7)))))))) H5))
 331 H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2:
 332 T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u
 333 t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3))
 334 (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T
 335 (THead (Flat Appl) v t0) (THead (Bind b) u t1))).(let H4 \def (eq_ind T
 336 (THead (Flat Appl) v t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
 337 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
 338 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
 339 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind
 340 b) u t1) H3) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
 341 u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Bind b) u
 342 t3)))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2:
 343 T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u
 344 t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2))
 345 (\lambda (t2: T).(eq T v2 (THead (Bind b) u t2))))))).(\lambda (t0:
 346 T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0
 347 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
 348 u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
 349 (H5: (eq T (THead (Flat Cast) v1 t0) (THead (Bind b) u t1))).(let H6 \def
 350 (eq_ind T (THead (Flat Cast) v1 t0) (\lambda (ee: T).(match ee in T return
 351 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 352 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
 353 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
 354 True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex2 T (\lambda (t3:
 355 T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat
 356 Cast) v2 t2) (THead (Bind b) u t3)))) H6)))))))))))) c y x H0))) H))))))).
 357 (* COMMENTS
 358 Initial nodes: 1975
 359 END *)
 360
 361 theorem sty0_gen_appl:
 362  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (x:
 363 T).((sty0 g c (THead (Flat Appl) u t1) x) \to (ex2 T (\lambda (t2: T).(sty0 g
 364 c t1 t2)) (\lambda (t2: T).(eq T x (THead (Flat Appl) u t2)))))))))
 365 \def
 366  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (x:
 367 T).(\lambda (H: (sty0 g c (THead (Flat Appl) u t1) x)).(insert_eq T (THead
 368 (Flat Appl) u t1) (\lambda (t: T).(sty0 g c t x)) (\lambda (_: T).(ex2 T
 369 (\lambda (t2: T).(sty0 g c t1 t2)) (\lambda (t2: T).(eq T x (THead (Flat
 370 Appl) u t2))))) (\lambda (y: T).(\lambda (H0: (sty0 g c y x)).(sty0_ind g
 371 (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Flat Appl)
 372 u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
 373 t0 (THead (Flat Appl) u t2)))))))) (\lambda (c0: C).(\lambda (n:
 374 nat).(\lambda (H1: (eq T (TSort n) (THead (Flat Appl) u t1))).(let H2 \def
 375 (eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_:
 376 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
 377 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H1) in
 378 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
 379 (TSort (next g n)) (THead (Flat Appl) u t2)))) H2))))) (\lambda (c0:
 380 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0
 381 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
 382 w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2:
 383 T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u
 384 t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5
 385 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
 386 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 387 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in
 388 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
 389 (lift (S i) O w) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (c0:
 390 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0
 391 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
 392 w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2:
 393 T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u
 394 t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5
 395 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
 396 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 397 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in
 398 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
 399 (lift (S i) O v) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (b:
 400 B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2:
 401 T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0 t2)).(\lambda (_: (((eq T t0
 402 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind
 403 b) v) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u
 404 t3))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Appl) u
 405 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee
 406 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
 407 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
 408 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
 409 False])])) I (THead (Flat Appl) u t1) H3) in (False_ind (ex2 T (\lambda (t3:
 410 T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) v t2) (THead
 411 (Flat Appl) u t3)))) H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda
 412 (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g c0 t0 t2)).(\lambda (H2: (((eq
 413 T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3))
 414 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3))))))).(\lambda (H3: (eq T
 415 (THead (Flat Appl) v t0) (THead (Flat Appl) u t1))).(let H4 \def (f_equal T T
 416 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
 417 \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t]))
 418 (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in ((let H5 \def
 419 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
 420 [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
 421 \Rightarrow t])) (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in
 422 (\lambda (H6: (eq T v u)).(let H7 \def (eq_ind T t0 (\lambda (t: T).((eq T t
 423 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3))
 424 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3)))))) H2 t1 H5) in (let H8
 425 \def (eq_ind T t0 (\lambda (t: T).(sty0 g c0 t t2)) H1 t1 H5) in (eq_ind_r T
 426 u (\lambda (t: T).(ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3:
 427 T).(eq T (THead (Flat Appl) t t2) (THead (Flat Appl) u t3))))) (ex_intro2 T
 428 (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl)
 429 u t2) (THead (Flat Appl) u t3))) t2 H8 (refl_equal T (THead (Flat Appl) u
 430 t2))) v H6))))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2:
 431 T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Flat Appl)
 432 u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
 433 v2 (THead (Flat Appl) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
 434 (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t1)) \to
 435 (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead
 436 (Flat Appl) u t3))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t0) (THead
 437 (Flat Appl) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t0) (\lambda
 438 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
 439 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 440 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
 441 (Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl
 442 \Rightarrow False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t1)
 443 H5) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3:
 444 T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Appl) u t3)))) H6))))))))))))
 445 c y x H0))) H)))))).
 446 (* COMMENTS
 447 Initial nodes: 1489
 448 END *)
 449
 450 theorem sty0_gen_cast:
 451  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall
 452 (x: T).((sty0 g c (THead (Flat Cast) v1 t1) x) \to (ex3_2 T T (\lambda (v2:
 453 T).(\lambda (_: T).(sty0 g c v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0
 454 g c t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Flat Cast) v2
 455 t2))))))))))
 456 \def
 457  \lambda (g: G).(\lambda (c: C).(\lambda (v1: T).(\lambda (t1: T).(\lambda
 458 (x: T).(\lambda (H: (sty0 g c (THead (Flat Cast) v1 t1) x)).(insert_eq T
 459 (THead (Flat Cast) v1 t1) (\lambda (t: T).(sty0 g c t x)) (\lambda (_:
 460 T).(ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c v1 v2))) (\lambda
 461 (_: T).(\lambda (t2: T).(sty0 g c t1 t2))) (\lambda (v2: T).(\lambda (t2:
 462 T).(eq T x (THead (Flat Cast) v2 t2)))))) (\lambda (y: T).(\lambda (H0: (sty0
 463 g c y x)).(sty0_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq
 464 T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_:
 465 T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2)))
 466 (\lambda (v2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) v2 t2)))))))))
 467 (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) (THead (Flat
 468 Cast) v1 t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee in
 469 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
 470 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast)
 471 v1 t1) H1) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g
 472 c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda
 473 (v2: T).(\lambda (t2: T).(eq T (TSort (next g n)) (THead (Flat Cast) v2
 474 t2))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i:
 475 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w:
 476 T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v (THead (Flat Cast) v1
 477 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g d v1 v2)))
 478 (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2))) (\lambda (v2: T).(\lambda
 479 (t2: T).(eq T w (THead (Flat Cast) v2 t2)))))))).(\lambda (H4: (eq T (TLRef
 480 i) (THead (Flat Cast) v1 t1))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee:
 481 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 482 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
 483 (THead (Flat Cast) v1 t1) H4) in (False_ind (ex3_2 T T (\lambda (v2:
 484 T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0
 485 g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T (lift (S i) O w) (THead
 486 (Flat Cast) v2 t2))))) H5))))))))))) (\lambda (c0: C).(\lambda (d:
 487 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind
 488 Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T
 489 v (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_:
 490 T).(sty0 g d v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2)))
 491 (\lambda (v2: T).(\lambda (t2: T).(eq T w (THead (Flat Cast) v2
 492 t2)))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) v1 t1))).(let H5
 493 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
 494 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 495 (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) v1 t1) H4) in
 496 (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2)))
 497 (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v2:
 498 T).(\lambda (t2: T).(eq T (lift (S i) O v) (THead (Flat Cast) v2 t2)))))
 499 H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0:
 500 T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0
 501 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T
 502 (\lambda (v2: T).(\lambda (_: T).(sty0 g (CHead c0 (Bind b) v) v1 v2)))
 503 (\lambda (_: T).(\lambda (t3: T).(sty0 g (CHead c0 (Bind b) v) t1 t3)))
 504 (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v2
 505 t3)))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Cast) v1
 506 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee
 507 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
 508 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
 509 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
 510 False])])) I (THead (Flat Cast) v1 t1) H3) in (False_ind (ex3_2 T T (\lambda
 511 (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t3:
 512 T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T (THead (Bind
 513 b) v t2) (THead (Flat Cast) v2 t3))))) H4)))))))))) (\lambda (c0: C).(\lambda
 514 (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0
 515 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T
 516 (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda
 517 (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead
 518 (Flat Cast) v2 t3)))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t0) (THead
 519 (Flat Cast) v1 t1))).(let H4 \def (eq_ind T (THead (Flat Appl) v t0) (\lambda
 520 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
 521 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 522 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
 523 (Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl
 524 \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat Cast) v1 t1)
 525 H3) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1
 526 v2))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2:
 527 T).(\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Flat Cast) v2
 528 t3))))) H4))))))))) (\lambda (c0: C).(\lambda (v0: T).(\lambda (v2:
 529 T).(\lambda (H1: (sty0 g c0 v0 v2)).(\lambda (H2: (((eq T v0 (THead (Flat
 530 Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1
 531 v3))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v3:
 532 T).(\lambda (t2: T).(eq T v2 (THead (Flat Cast) v3 t2)))))))).(\lambda (t0:
 533 T).(\lambda (t2: T).(\lambda (H3: (sty0 g c0 t0 t2)).(\lambda (H4: (((eq T t0
 534 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_:
 535 T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3)))
 536 (\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v3
 537 t3)))))))).(\lambda (H5: (eq T (THead (Flat Cast) v0 t0) (THead (Flat Cast)
 538 v1 t1))).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return
 539 (\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0
 540 | (THead _ t _) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast)
 541 v1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return
 542 (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0
 543 | (THead _ _ t) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast)
 544 v1 t1) H5) in (\lambda (H8: (eq T v0 v1)).(let H9 \def (eq_ind T t0 (\lambda
 545 (t: T).((eq T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3:
 546 T).(\lambda (_: T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0
 547 g c0 t1 t3))) (\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast)
 548 v3 t3))))))) H4 t1 H7) in (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g
 549 c0 t t2)) H3 t1 H7) in (let H11 \def (eq_ind T v0 (\lambda (t: T).((eq T t
 550 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_:
 551 T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3)))
 552 (\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Flat Cast) v3 t3))))))) H2
 553 v1 H8) in (let H12 \def (eq_ind T v0 (\lambda (t: T).(sty0 g c0 t v2)) H1 v1
 554 H8) in (ex3_2_intro T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3)))
 555 (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v3:
 556 T).(\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Cast) v3
 557 t3)))) v2 t2 H12 H10 (refl_equal T (THead (Flat Cast) v2 t2)))))))))
 558 H6)))))))))))) c y x H0))) H)))))).
 559 (* COMMENTS
 560 Initial nodes: 1855
 561 END *)
 562