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