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