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