matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/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/ex1/props".
  18
  19 include "ex1/defs.ma".
  20
  21 include "ty3/fwd.ma".
  22
  23 include "pc3/fwd.ma".
  24
  25 include "nf2/pr3.ma".
  26
  27 include "nf2/props.ma".
  28
  29 include "arity/defs.ma".
  30
  31 include "leq/props.ma".
  32
  33 theorem ex1__leq_sort_SS:
  34  \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc
  35 g (asucc g (ASort (S (S k)) n))))))
  36 \def
  37  \lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g
  38 (asucc g (ASort (S (S k)) n)))))).
  39
  40 theorem ex1_arity:
  41  \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
  42 \def
  43  \lambda (g: G).(arity_appl g (CHead (CHead (CHead (CSort O) (Bind Abst)
  44 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef O) (ASort (S
  45 (S O)) O) (arity_abst g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
  46 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind
  47 Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) O (getl_refl Abst (CHead
  48 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O))
  49 (ASort (S (S O)) O) (arity_abst g (CHead (CHead (CSort O) (Bind Abst) (TSort
  50 O)) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O)
  51 O (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O)) (asucc g
  52 (ASort (S (S O)) O)) (arity_repl g (CHead (CSort O) (Bind Abst) (TSort O))
  53 (TSort O) (ASort O O) (arity_sort g (CHead (CSort O) (Bind Abst) (TSort O))
  54 O) (asucc g (asucc g (ASort (S (S O)) O))) (ex1__leq_sort_SS g O O)))) (THead
  55 (Bind Abst) (TLRef (S (S O))) (TSort O)) (ASort O O) (arity_head g (CHead
  56 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
  57 Abst) (TLRef O)) (TLRef (S (S O))) (ASort (S (S O)) O) (arity_abst g (CHead
  58 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
  59 Abst) (TLRef O)) (CSort O) (TSort O) (S (S O)) (getl_clear_bind Abst (CHead
  60 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
  61 Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
  62 (TSort O)) (TLRef O) (clear_bind Abst (CHead (CHead (CSort O) (Bind Abst)
  63 (TSort O)) (Bind Abst) (TSort O)) (TLRef O)) (CHead (CSort O) (Bind Abst)
  64 (TSort O)) (S O) (getl_head (Bind Abst) O (CHead (CSort O) (Bind Abst) (TSort
  65 O)) (CHead (CSort O) (Bind Abst) (TSort O)) (getl_refl Abst (CSort O) (TSort
  66 O)) (TSort O))) (asucc g (ASort (S (S O)) O)) (arity_repl g (CSort O) (TSort
  67 O) (ASort O O) (arity_sort g (CSort O) O) (asucc g (asucc g (ASort (S (S O))
  68 O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead
  69 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
  70 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
  71
  72 theorem ex1_ty3:
  73  \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P:
  74 Prop).P)))
  75 \def
  76  \lambda (g: G).(\lambda (u: T).(\lambda (H: (ty3 g (CHead (CHead (CHead
  77 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
  78 O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort
  79 O))) u)).(\lambda (P: Prop).(ex3_2_ind T T (\lambda (u0: T).(\lambda (t:
  80 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
  81 (TSort O)) (Bind Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind
  82 Abst) u0 t)) u))) (\lambda (u0: T).(\lambda (t: T).(ty3 g (CHead (CHead
  83 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
  84 (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) (THead (Bind Abst)
  85 u0 t)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort
  86 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
  87 (TLRef O) u0))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 (CHead
  88 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
  89 Abst) (TLRef O)) (THead (Flat Appl) (TLRef O) (THead (Bind Abst) x0 x1))
  90 u)).(\lambda (H1: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
  91 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef
  92 (S (S O))) (TSort O)) (THead (Bind Abst) x0 x1))).(\lambda (H2: (ty3 g (CHead
  93 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
  94 Abst) (TLRef O)) (TLRef O) x0)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda
  95 (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
  96 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O t) x0))))
  97 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead
  98 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
  99 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 100 (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
 101 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 102 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0))))
 103 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead
 104 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 105 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 106 (t: T).(ty3 g e u0 t))))) P (\lambda (H3: (ex3_3 C T T (\lambda (_:
 107 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 108 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
 109 t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead
 110 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 111 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
 112 T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_:
 113 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 114 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
 115 t) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead
 116 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 117 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
 118 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2: C).(\lambda (x3:
 119 T).(\lambda (x4: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
 120 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O
 121 x4) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort O) (Bind Abst)
 122 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind
 123 Abbr) x3))).(\lambda (_: (ty3 g x2 x3 x4)).(ex4_3_ind T T T (\lambda (t2:
 124 T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 125 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind
 126 Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1))))) (\lambda (_:
 127 T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CSort O)
 128 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
 129 (S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
 130 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 131 (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O)
 132 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead (CHead
 133 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 134 Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda (x5:
 135 T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (_: (pc3 (CHead (CHead (CHead
 136 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 137 O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0
 138 x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
 139 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
 140 x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst)
 141 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef
 142 (S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead
 143 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 144 O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_:
 145 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 146 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 147 O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S
 148 O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
 149 O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e:
 150 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda
 151 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O)
 152 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S
 153 (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
 154 T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 155 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0)))))
 156 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
 157 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
 158 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 159 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda
 160 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
 161 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 162 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 163 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
 164 T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 165 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))))
 166 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead
 167 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 168 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
 169 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
 170 T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
 171 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 172 O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort
 173 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 174 (CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def
 175 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 176 (TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
 177 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 178 (CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
 179 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 180 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P
 181 (\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind
 182 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x8
 183 (Bind Abbr) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda
 184 (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 185 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 186 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
 187 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
 188 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead
 189 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 190 O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 191 Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead
 192 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 193 Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18)))))
 194 H15)))))))) H11)) (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
 195 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 196 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0)
 197 x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O))
 198 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 199 (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda
 200 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_:
 201 C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 202 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 203 O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S
 204 (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 205 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
 206 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8:
 207 C).(\lambda (x9: T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead
 208 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 209 O)) (lift (S (S (S O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead
 210 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 211 Abst) (TLRef O)) (CHead x8 (Bind Abst) x9))).(\lambda (_: (ty3 g x8 x9
 212 x10)).(let H15 \def (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort
 213 O)) (Bind Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O))
 214 (getl_gen_S (Bind Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 215 Abst) (TSort O)) (CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind
 216 C (\lambda (e: C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort
 217 O)) (Bind Abst) (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst)
 218 x9))) P (\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O)
 219 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x
 220 (CHead x8 (Bind Abst) x9))).(let H18 \def (eq_ind C (CHead x2 (Bind Abbr) x3)
 221 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 222 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 223 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
 224 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
 225 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead
 226 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 227 O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 228 Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead
 229 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 230 Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H18)))))
 231 H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst)
 232 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S O))
 233 H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst)
 234 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
 235 (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) (\lambda (H3: (ex3_3 C T
 236 T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
 237 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 238 O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
 239 T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 240 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
 241 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T
 242 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
 243 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 244 O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
 245 T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 246 (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e:
 247 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2:
 248 C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4: (pc3 (CHead (CHead (CHead
 249 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 250 O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort
 251 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 252 (CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3 x4)).(ex4_3_ind T T T
 253 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead
 254 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 255 O)) (THead (Bind Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1)))))
 256 (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead
 257 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 258 O)) (TLRef (S (S O))) t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_:
 259 T).(ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 260 Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort
 261 O) t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead
 262 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 263 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) t2 t0)))) P (\lambda
 264 (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (H7: (pc3 (CHead (CHead
 265 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
 266 (TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0
 267 x1))).(\lambda (H8: (ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
 268 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
 269 x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead (CSort O) (Bind Abst)
 270 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind Abst) (TLRef
 271 (S (S O)))) (TSort O) x5)).(\lambda (_: (ty3 g (CHead (CHead (CHead (CHead
 272 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 273 O)) (Bind Abst) (TLRef (S (S O)))) x5 x7)).(or_ind (ex3_3 C T T (\lambda (_:
 274 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind
 275 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 276 O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S
 277 O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
 278 O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e:
 279 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda
 280 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O)
 281 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S
 282 (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
 283 T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 284 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0)))))
 285 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
 286 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
 287 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 288 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda
 289 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
 290 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 291 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 292 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
 293 T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 294 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))))
 295 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead
 296 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 297 Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
 298 T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
 299 T).(\lambda (x10: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind
 300 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 301 O))) O x10) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort
 302 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 303 (CHead x8 (Bind Abbr) x9))).(\lambda (_: (ty3 g x8 x9 x10)).(let H15 \def
 304 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 305 (TSort O)) (CHead x8 (Bind Abbr) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
 306 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 307 (CHead x8 (Bind Abbr) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
 308 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 309 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abbr) x9))) P
 310 (\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind
 311 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8
 312 (Bind Abbr) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C
 313 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _)
 314 \Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O)
 315 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 316 (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 317 Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead
 318 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 319 Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C
 320 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 321 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3)
 322 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 323 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind
 324 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O)
 325 (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 326 (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda
 327 (H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 328 (TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6
 329 (TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead
 330 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 331 Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def
 332 (eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort
 333 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def
 334 (eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abbr) x9))) H17 (CHead
 335 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst)
 336 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort
 337 O)) x (TSort O) O H16))) in (let H25 \def (eq_ind C (CHead x8 (Bind Abbr) x9)
 338 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 339 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 340 (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_:
 341 B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void
 342 \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CSort O)
 343 (Bind Abst) (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abbr)
 344 x9) (TSort O) H24)) in (False_ind P H25)))))))) H18))))) H15)))))))) H11))
 345 (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
 346 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 347 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda
 348 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead
 349 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 350 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 351 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0:
 352 T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 353 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0)
 354 x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O))
 355 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 356 (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda
 357 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x8: C).(\lambda (x9:
 358 T).(\lambda (x10: T).(\lambda (H12: (pc3 (CHead (CHead (CHead (CSort O) (Bind
 359 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S
 360 O))) O x9) x6)).(\lambda (H13: (getl (S (S O)) (CHead (CHead (CHead (CSort O)
 361 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead
 362 x8 (Bind Abst) x9))).(\lambda (H14: (ty3 g x8 x9 x10)).(let H15 \def
 363 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 364 (TSort O)) (CHead x8 (Bind Abst) x9) (r (Bind Abst) (S O)) (getl_gen_S (Bind
 365 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 366 (CHead x8 (Bind Abst) x9) (TLRef O) (S O) H13)) in (ex2_ind C (\lambda (e:
 367 C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 368 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x8 (Bind Abst) x9))) P
 369 (\lambda (x: C).(\lambda (H16: (drop (S O) O (CHead (CHead (CSort O) (Bind
 370 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H17: (clear x (CHead x8
 371 (Bind Abst) x9))).(let H18 \def (f_equal C C (\lambda (e: C).(match e in C
 372 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _)
 373 \Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O)
 374 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 375 (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 376 Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead
 377 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 378 Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H19 \def (f_equal C
 379 T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 380 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3)
 381 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 382 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind
 383 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O)
 384 (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 385 (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in (\lambda
 386 (H20: (eq C x2 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 387 (TSort O)))).(let H21 \def (eq_ind T x3 (\lambda (t: T).(ty3 g x2 t x4)) H6
 388 (TLRef O) H19) in (let H22 \def (eq_ind T x3 (\lambda (t: T).(pc3 (CHead
 389 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 390 Abst) (TLRef O)) (lift (S O) O t) x0)) H4 (TLRef O) H19) in (let H23 \def
 391 (eq_ind C x2 (\lambda (c: C).(ty3 g c (TLRef O) x4)) H21 (CHead (CHead (CSort
 392 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H20) in (let H24 \def
 393 (eq_ind_r C x (\lambda (c: C).(clear c (CHead x8 (Bind Abst) x9))) H17 (CHead
 394 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst)
 395 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort
 396 O)) x (TSort O) O H16))) in (let H25 \def (f_equal C C (\lambda (e: C).(match
 397 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow x8 | (CHead c _
 398 _) \Rightarrow c])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst)
 399 (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O)
 400 H24)) in ((let H26 \def (f_equal C T (\lambda (e: C).(match e in C return
 401 (\lambda (_: C).T) with [(CSort _) \Rightarrow x9 | (CHead _ _ t) \Rightarrow
 402 t])) (CHead x8 (Bind Abst) x9) (CHead (CSort O) (Bind Abst) (TSort O))
 403 (clear_gen_bind Abst (CSort O) (CHead x8 (Bind Abst) x9) (TSort O) H24)) in
 404 (\lambda (H27: (eq C x8 (CSort O))).(let H28 \def (eq_ind T x9 (\lambda (t:
 405 T).(ty3 g x8 t x10)) H14 (TSort O) H26) in (let H29 \def (eq_ind T x9
 406 (\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 407 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6))
 408 H12 (TSort O) H26) in (let H30 \def (eq_ind C x8 (\lambda (c: C).(ty3 g c
 409 (TSort O) x10)) H28 (CSort O) H27) in (or_ind (ex3_3 C T T (\lambda (_:
 410 C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst)
 411 (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e:
 412 C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind
 413 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda
 414 (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T
 415 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O)
 416 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4))))
 417 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort
 418 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0)))))
 419 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P
 420 (\lambda (H31: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
 421 T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 422 (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
 423 T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
 424 O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
 425 (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
 426 T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 427 Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0:
 428 T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 429 (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda
 430 (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x11: C).(\lambda (x12:
 431 T).(\lambda (x13: T).(\lambda (_: (pc3 (CHead (CHead (CSort O) (Bind Abst)
 432 (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x13) x4)).(\lambda (H33:
 433 (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 434 (CHead x11 (Bind Abbr) x12))).(\lambda (_: (ty3 g x11 x12 x13)).(let H35 \def
 435 (eq_ind C (CHead x11 (Bind Abbr) x12) (\lambda (ee: C).(match ee in C return
 436 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
 437 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
 438 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
 439 True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _)
 440 \Rightarrow False])])) I (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 441 Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O) (Bind Abst) (TSort O))
 442 (CHead x11 (Bind Abbr) x12) (TSort O) (getl_gen_O (CHead (CHead (CSort O)
 443 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abbr) x12)
 444 H33))) in (False_ind P H35)))))))) H31)) (\lambda (H31: (ex3_3 C T T (\lambda
 445 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) (Bind
 446 Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) (\lambda (e:
 447 C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind
 448 Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) (\lambda
 449 (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T
 450 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O)
 451 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4))))
 452 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort
 453 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0)))))
 454 (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda
 455 (x11: C).(\lambda (x12: T).(\lambda (x13: T).(\lambda (H32: (pc3 (CHead
 456 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O
 457 x12) x4)).(\lambda (H33: (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort
 458 O)) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12))).(\lambda (H34: (ty3
 459 g x11 x12 x13)).(let H35 \def (f_equal C C (\lambda (e: C).(match e in C
 460 return (\lambda (_: C).C) with [(CSort _) \Rightarrow x11 | (CHead c _ _)
 461 \Rightarrow c])) (CHead x11 (Bind Abst) x12) (CHead (CHead (CSort O) (Bind
 462 Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O)
 463 (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O) (getl_gen_O
 464 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead
 465 x11 (Bind Abst) x12) H33))) in ((let H36 \def (f_equal C T (\lambda (e:
 466 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x12 |
 467 (CHead _ _ t) \Rightarrow t])) (CHead x11 (Bind Abst) x12) (CHead (CHead
 468 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst
 469 (CHead (CSort O) (Bind Abst) (TSort O)) (CHead x11 (Bind Abst) x12) (TSort O)
 470 (getl_gen_O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort
 471 O)) (CHead x11 (Bind Abst) x12) H33))) in (\lambda (H37: (eq C x11 (CHead
 472 (CSort O) (Bind Abst) (TSort O)))).(let H38 \def (eq_ind T x12 (\lambda (t:
 473 T).(ty3 g x11 t x13)) H34 (TSort O) H36) in (let H39 \def (eq_ind T x12
 474 (\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 475 Abst) (TSort O)) (lift (S O) O t) x4)) H32 (TSort O) H36) in (let H40 \def
 476 (eq_ind C x11 (\lambda (c: C).(ty3 g c (TSort O) x13)) H38 (CHead (CSort O)
 477 (Bind Abst) (TSort O)) H37) in (and_ind (pc3 (CHead (CHead (CHead (CSort O)
 478 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
 479 (S (S O))) x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead
 480 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst)
 481 (TLRef O)) (Bind b) u0) x5 x1))) P (\lambda (H41: (pc3 (CHead (CHead (CHead
 482 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 483 O)) (TLRef (S (S O))) x0)).(\lambda (_: ((\forall (b: B).(\forall (u0:
 484 T).(pc3 (CHead (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 485 Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind b) u0) x5 x1))))).(let H43 \def
 486 (eq_ind T (lift (S O) O (TLRef O)) (\lambda (t: T).(pc3 (CHead (CHead (CHead
 487 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 488 O)) (TLRef (S (S O))) t)) (pc3_t x0 (CHead (CHead (CHead (CSort O) (Bind
 489 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S
 490 O))) H41 (lift (S O) O (TLRef O)) (ex2_sym T (pr3 (CHead (CHead (CHead (CSort
 491 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift
 492 (S O) O (TLRef O))) (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
 493 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x0) H22)) (TLRef (plus O (S
 494 O))) (lift_lref_ge O (S O) O (le_n O))) in (let H44 \def H43 in (ex2_ind T
 495 (\lambda (t: T).(pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 496 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) t)) (\lambda
 497 (t: T).(pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 498 (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) t)) P (\lambda (x14:
 499 T).(\lambda (H45: (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 500 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
 501 x14)).(\lambda (H46: (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort
 502 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x14)).(let
 503 H47 \def (eq_ind_r T x14 (\lambda (t: T).(eq T (TLRef (S (S O))) t))
 504 (nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 505 Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x14 H45
 506 (nf2_lref_abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 507 Abst) (TSort O)) (Bind Abst) (TLRef O)) (CSort O) (TSort O) (S (S O))
 508 (getl_clear_bind Abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 509 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead (CHead (CSort O) (Bind
 510 Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O) (clear_bind Abst (CHead
 511 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (TLRef O))
 512 (CHead (CSort O) (Bind Abst) (TSort O)) (S O) (getl_head (Bind Abst) O (CHead
 513 (CSort O) (Bind Abst) (TSort O)) (CHead (CSort O) (Bind Abst) (TSort O))
 514 (getl_refl Abst (CSort O) (TSort O)) (TSort O))))) (TLRef (S O))
 515 (nf2_pr3_unfold (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 516 Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S O)) x14 H46 (nf2_lref_abst
 517 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
 518 (Bind Abst) (TLRef O)) (CHead (CSort O) (Bind Abst) (TSort O)) (TSort O) (S
 519 O) (getl_head (Bind Abst) O (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 520 (Bind Abst) (TSort O)) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 521 Abst) (TSort O)) (getl_refl Abst (CHead (CSort O) (Bind Abst) (TSort O))
 522 (TSort O)) (TLRef O))))) in (let H48 \def (eq_ind T (TLRef (S (S O)))
 523 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
 524 \Rightarrow False | (TLRef n) \Rightarrow (match n in nat return (\lambda (_:
 525 nat).Prop) with [O \Rightarrow False | (S n0) \Rightarrow (match n0 in nat
 526 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
 527 True])]) | (THead _ _ _) \Rightarrow False])) I (TLRef (S O)) H47) in
 528 (False_ind P H48)))))) H44))))) (pc3_gen_abst (CHead (CHead (CHead (CSort O)
 529 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
 530 (S (S O))) x0 x5 x1 H7))))))) H35)))))))) H31)) (ty3_gen_lref g (CHead (CHead
 531 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x4 O H23)))))))
 532 H25)))))))) H18))))) H15)))))))) H11)) (ty3_gen_lref g (CHead (CHead (CHead
 533 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef
 534 O)) x6 (S (S O)) H8))))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort
 535 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O))
 536 (TLRef (S (S O))) (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3))
 537 (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind
 538 Abst) (TSort O)) (Bind Abst) (TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead
 539 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind
 540 Abst) (TLRef O)) (TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u
 541 H))))).
 542