matita/matita/contribs/lambdadelta/basic_1/lift1/drop1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1/lift/props.ma".
  18
  19 include "basic_1/drop1/defs.ma".
  20
  21 theorem lift1_lift1:
  22  \forall (is1: PList).(\forall (is2: PList).(\forall (t: T).(eq T (lift1 is1
  23 (lift1 is2 t)) (lift1 (papp is1 is2) t))))
  24 \def
  25  \lambda (is1: PList).(let TMP_5 \def (\lambda (p: PList).(\forall (is2:
  26 PList).(\forall (t: T).(let TMP_1 \def (lift1 is2 t) in (let TMP_2 \def
  27 (lift1 p TMP_1) in (let TMP_3 \def (papp p is2) in (let TMP_4 \def (lift1
  28 TMP_3 t) in (eq T TMP_2 TMP_4)))))))) in (let TMP_7 \def (\lambda (is2:
  29 PList).(\lambda (t: T).(let TMP_6 \def (lift1 is2 t) in (refl_equal T
  30 TMP_6)))) in (let TMP_15 \def (\lambda (n: nat).(\lambda (n0: nat).(\lambda
  31 (p: PList).(\lambda (H: ((\forall (is2: PList).(\forall (t: T).(eq T (lift1 p
  32 (lift1 is2 t)) (lift1 (papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t:
  33 T).(let TMP_8 \def (lift1 is2 t) in (let TMP_9 \def (lift1 p TMP_8) in (let
  34 TMP_10 \def (papp p is2) in (let TMP_11 \def (lift1 TMP_10 t) in (let TMP_12
  35 \def (refl_equal nat n) in (let TMP_13 \def (refl_equal nat n0) in (let
  36 TMP_14 \def (H is2 t) in (f_equal3 nat nat T T lift n n n0 n0 TMP_9 TMP_11
  37 TMP_12 TMP_13 TMP_14)))))))))))))) in (PList_ind TMP_5 TMP_7 TMP_15 is1)))).
  38
  39 theorem lift1_xhg:
  40  \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t))
  41 (lift (S O) O (lift1 hds t))))
  42 \def
  43  \lambda (hds: PList).(let TMP_8 \def (\lambda (p: PList).(\forall (t:
  44 T).(let TMP_1 \def (Ss p) in (let TMP_2 \def (S O) in (let TMP_3 \def (lift
  45 TMP_2 O t) in (let TMP_4 \def (lift1 TMP_1 TMP_3) in (let TMP_5 \def (S O) in
  46 (let TMP_6 \def (lift1 p t) in (let TMP_7 \def (lift TMP_5 O TMP_6) in (eq T
  47 TMP_4 TMP_7)))))))))) in (let TMP_11 \def (\lambda (t: T).(let TMP_9 \def (S
  48 O) in (let TMP_10 \def (lift TMP_9 O t) in (refl_equal T TMP_10)))) in (let
  49 TMP_67 \def (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda
  50 (H: ((\forall (t: T).(eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O
  51 (lift1 p t)))))).(\lambda (t: T).(let TMP_12 \def (S O) in (let TMP_13 \def
  52 (lift1 p t) in (let TMP_14 \def (lift TMP_12 O TMP_13) in (let TMP_21 \def
  53 (\lambda (t0: T).(let TMP_15 \def (S d) in (let TMP_16 \def (lift h TMP_15
  54 t0) in (let TMP_17 \def (S O) in (let TMP_18 \def (lift1 p t) in (let TMP_19
  55 \def (lift h d TMP_18) in (let TMP_20 \def (lift TMP_17 O TMP_19) in (eq T
  56 TMP_16 TMP_20)))))))) in (let TMP_22 \def (S O) in (let TMP_23 \def (plus
  57 TMP_22 d) in (let TMP_32 \def (\lambda (n: nat).(let TMP_24 \def (S O) in
  58 (let TMP_25 \def (lift1 p t) in (let TMP_26 \def (lift TMP_24 O TMP_25) in
  59 (let TMP_27 \def (lift h n TMP_26) in (let TMP_28 \def (S O) in (let TMP_29
  60 \def (lift1 p t) in (let TMP_30 \def (lift h d TMP_29) in (let TMP_31 \def
  61 (lift TMP_28 O TMP_30) in (eq T TMP_27 TMP_31)))))))))) in (let TMP_33 \def
  62 (S O) in (let TMP_34 \def (lift1 p t) in (let TMP_35 \def (lift h d TMP_34)
  63 in (let TMP_36 \def (lift TMP_33 O TMP_35) in (let TMP_41 \def (\lambda (t0:
  64 T).(let TMP_37 \def (S O) in (let TMP_38 \def (lift1 p t) in (let TMP_39 \def
  65 (lift h d TMP_38) in (let TMP_40 \def (lift TMP_37 O TMP_39) in (eq T t0
  66 TMP_40)))))) in (let TMP_42 \def (S O) in (let TMP_43 \def (lift1 p t) in
  67 (let TMP_44 \def (lift h d TMP_43) in (let TMP_45 \def (lift TMP_42 O TMP_44)
  68 in (let TMP_46 \def (refl_equal T TMP_45) in (let TMP_47 \def (S O) in (let
  69 TMP_48 \def (plus TMP_47 d) in (let TMP_49 \def (S O) in (let TMP_50 \def
  70 (lift1 p t) in (let TMP_51 \def (lift TMP_49 O TMP_50) in (let TMP_52 \def
  71 (lift h TMP_48 TMP_51) in (let TMP_53 \def (lift1 p t) in (let TMP_54 \def (S
  72 O) in (let TMP_55 \def (le_O_n d) in (let TMP_56 \def (lift_d TMP_53 h TMP_54
  73 d O TMP_55) in (let TMP_57 \def (eq_ind_r T TMP_36 TMP_41 TMP_46 TMP_52
  74 TMP_56) in (let TMP_58 \def (S d) in (let TMP_59 \def (S d) in (let TMP_60
  75 \def (refl_equal nat TMP_59) in (let TMP_61 \def (eq_ind nat TMP_23 TMP_32
  76 TMP_57 TMP_58 TMP_60) in (let TMP_62 \def (Ss p) in (let TMP_63 \def (S O) in
  77 (let TMP_64 \def (lift TMP_63 O t) in (let TMP_65 \def (lift1 TMP_62 TMP_64)
  78 in (let TMP_66 \def (H t) in (eq_ind_r T TMP_14 TMP_21 TMP_61 TMP_65
  79 TMP_66))))))))))))))))))))))))))))))))))))))))))) in (PList_ind TMP_8 TMP_11
  80 TMP_67 hds)))).
  81
  82 theorem lifts1_xhg:
  83  \forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (Ss hds) (lifts
  84 (S O) O ts)) (lifts (S O) O (lifts1 hds ts))))
  85 \def
  86  \lambda (hds: PList).(\lambda (ts: TList).(let TMP_8 \def (\lambda (t:
  87 TList).(let TMP_1 \def (Ss hds) in (let TMP_2 \def (S O) in (let TMP_3 \def
  88 (lifts TMP_2 O t) in (let TMP_4 \def (lifts1 TMP_1 TMP_3) in (let TMP_5 \def
  89 (S O) in (let TMP_6 \def (lifts1 hds t) in (let TMP_7 \def (lifts TMP_5 O
  90 TMP_6) in (eq TList TMP_4 TMP_7))))))))) in (let TMP_9 \def (refl_equal TList
  91 TNil) in (let TMP_59 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
  92 (eq TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds
  93 t0)))).(let TMP_10 \def (S O) in (let TMP_11 \def (lift1 hds t) in (let
  94 TMP_12 \def (lift TMP_10 O TMP_11) in (let TMP_25 \def (\lambda (t1: T).(let
  95 TMP_13 \def (Ss hds) in (let TMP_14 \def (S O) in (let TMP_15 \def (lifts
  96 TMP_14 O t0) in (let TMP_16 \def (lifts1 TMP_13 TMP_15) in (let TMP_17 \def
  97 (TCons t1 TMP_16) in (let TMP_18 \def (S O) in (let TMP_19 \def (lift1 hds t)
  98 in (let TMP_20 \def (lift TMP_18 O TMP_19) in (let TMP_21 \def (S O) in (let
  99 TMP_22 \def (lifts1 hds t0) in (let TMP_23 \def (lifts TMP_21 O TMP_22) in
 100 (let TMP_24 \def (TCons TMP_20 TMP_23) in (eq TList TMP_17
 101 TMP_24)))))))))))))) in (let TMP_26 \def (S O) in (let TMP_27 \def (lifts1
 102 hds t0) in (let TMP_28 \def (lifts TMP_26 O TMP_27) in (let TMP_40 \def
 103 (\lambda (t1: TList).(let TMP_29 \def (S O) in (let TMP_30 \def (lift1 hds t)
 104 in (let TMP_31 \def (lift TMP_29 O TMP_30) in (let TMP_32 \def (TCons TMP_31
 105 t1) in (let TMP_33 \def (S O) in (let TMP_34 \def (lift1 hds t) in (let
 106 TMP_35 \def (lift TMP_33 O TMP_34) in (let TMP_36 \def (S O) in (let TMP_37
 107 \def (lifts1 hds t0) in (let TMP_38 \def (lifts TMP_36 O TMP_37) in (let
 108 TMP_39 \def (TCons TMP_35 TMP_38) in (eq TList TMP_32 TMP_39))))))))))))) in
 109 (let TMP_41 \def (S O) in (let TMP_42 \def (lift1 hds t) in (let TMP_43 \def
 110 (lift TMP_41 O TMP_42) in (let TMP_44 \def (S O) in (let TMP_45 \def (lifts1
 111 hds t0) in (let TMP_46 \def (lifts TMP_44 O TMP_45) in (let TMP_47 \def
 112 (TCons TMP_43 TMP_46) in (let TMP_48 \def (refl_equal TList TMP_47) in (let
 113 TMP_49 \def (Ss hds) in (let TMP_50 \def (S O) in (let TMP_51 \def (lifts
 114 TMP_50 O t0) in (let TMP_52 \def (lifts1 TMP_49 TMP_51) in (let TMP_53 \def
 115 (eq_ind_r TList TMP_28 TMP_40 TMP_48 TMP_52 H) in (let TMP_54 \def (Ss hds)
 116 in (let TMP_55 \def (S O) in (let TMP_56 \def (lift TMP_55 O t) in (let
 117 TMP_57 \def (lift1 TMP_54 TMP_56) in (let TMP_58 \def (lift1_xhg hds t) in
 118 (eq_ind_r T TMP_12 TMP_25 TMP_53 TMP_57 TMP_58))))))))))))))))))))))))))))))
 119 in (TList_ind TMP_8 TMP_9 TMP_59 ts))))).
 120
 121 theorem lift1_free:
 122  \forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds
 123 (lift (S i) O t)) (lift (S (trans hds i)) O (lift1 (ptrans hds i) t)))))
 124 \def
 125  \lambda (hds: PList).(let TMP_9 \def (\lambda (p: PList).(\forall (i:
 126 nat).(\forall (t: T).(let TMP_1 \def (S i) in (let TMP_2 \def (lift TMP_1 O
 127 t) in (let TMP_3 \def (lift1 p TMP_2) in (let TMP_4 \def (trans p i) in (let
 128 TMP_5 \def (S TMP_4) in (let TMP_6 \def (ptrans p i) in (let TMP_7 \def
 129 (lift1 TMP_6 t) in (let TMP_8 \def (lift TMP_5 O TMP_7) in (eq T TMP_3
 130 TMP_8)))))))))))) in (let TMP_12 \def (\lambda (i: nat).(\lambda (t: T).(let
 131 TMP_10 \def (S i) in (let TMP_11 \def (lift TMP_10 O t) in (refl_equal T
 132 TMP_11))))) in (let TMP_262 \def (\lambda (h: nat).(\lambda (d: nat).(\lambda
 133 (hds0: PList).(\lambda (H: ((\forall (i: nat).(\forall (t: T).(eq T (lift1
 134 hds0 (lift (S i) O t)) (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i)
 135 t))))))).(\lambda (i: nat).(\lambda (t: T).(let TMP_13 \def (trans hds0 i) in
 136 (let TMP_14 \def (S TMP_13) in (let TMP_15 \def (ptrans hds0 i) in (let
 137 TMP_16 \def (lift1 TMP_15 t) in (let TMP_17 \def (lift TMP_14 O TMP_16) in
 138 (let TMP_33 \def (\lambda (t0: T).(let TMP_18 \def (lift h d t0) in (let
 139 TMP_19 \def (trans hds0 i) in (let TMP_20 \def (blt TMP_19 d) in (let TMP_22
 140 \def (match TMP_20 with [true \Rightarrow (trans hds0 i) | false \Rightarrow
 141 (let TMP_21 \def (trans hds0 i) in (plus TMP_21 h))]) in (let TMP_23 \def (S
 142 TMP_22) in (let TMP_24 \def (trans hds0 i) in (let TMP_25 \def (blt TMP_24 d)
 143 in (let TMP_30 \def (match TMP_25 with [true \Rightarrow (let TMP_26 \def
 144 (trans hds0 i) in (let TMP_27 \def (S TMP_26) in (let TMP_28 \def (minus d
 145 TMP_27) in (let TMP_29 \def (ptrans hds0 i) in (PCons h TMP_28 TMP_29))))) |
 146 false \Rightarrow (ptrans hds0 i)]) in (let TMP_31 \def (lift1 TMP_30 t) in
 147 (let TMP_32 \def (lift TMP_23 O TMP_31) in (eq T TMP_18 TMP_32)))))))))))) in
 148 (let TMP_34 \def (trans hds0 i) in (let TMP_35 \def (blt TMP_34 d) in (let
 149 TMP_52 \def (\lambda (b: bool).(let TMP_36 \def (trans hds0 i) in (let TMP_37
 150 \def (S TMP_36) in (let TMP_38 \def (ptrans hds0 i) in (let TMP_39 \def
 151 (lift1 TMP_38 t) in (let TMP_40 \def (lift TMP_37 O TMP_39) in (let TMP_41
 152 \def (lift h d TMP_40) in (let TMP_43 \def (match b with [true \Rightarrow
 153 (trans hds0 i) | false \Rightarrow (let TMP_42 \def (trans hds0 i) in (plus
 154 TMP_42 h))]) in (let TMP_44 \def (S TMP_43) in (let TMP_49 \def (match b with
 155 [true \Rightarrow (let TMP_45 \def (trans hds0 i) in (let TMP_46 \def (S
 156 TMP_45) in (let TMP_47 \def (minus d TMP_46) in (let TMP_48 \def (ptrans hds0
 157 i) in (PCons h TMP_47 TMP_48))))) | false \Rightarrow (ptrans hds0 i)]) in
 158 (let TMP_50 \def (lift1 TMP_49 t) in (let TMP_51 \def (lift TMP_44 O TMP_50)
 159 in (eq T TMP_41 TMP_51))))))))))))) in (let TMP_256 \def (\lambda (x_x:
 160 bool).(let TMP_69 \def (\lambda (b: bool).((eq bool (blt (trans hds0 i) d) b)
 161 \to (let TMP_53 \def (trans hds0 i) in (let TMP_54 \def (S TMP_53) in (let
 162 TMP_55 \def (ptrans hds0 i) in (let TMP_56 \def (lift1 TMP_55 t) in (let
 163 TMP_57 \def (lift TMP_54 O TMP_56) in (let TMP_58 \def (lift h d TMP_57) in
 164 (let TMP_60 \def (match b with [true \Rightarrow (trans hds0 i) | false
 165 \Rightarrow (let TMP_59 \def (trans hds0 i) in (plus TMP_59 h))]) in (let
 166 TMP_61 \def (S TMP_60) in (let TMP_66 \def (match b with [true \Rightarrow
 167 (let TMP_62 \def (trans hds0 i) in (let TMP_63 \def (S TMP_62) in (let TMP_64
 168 \def (minus d TMP_63) in (let TMP_65 \def (ptrans hds0 i) in (PCons h TMP_64
 169 TMP_65))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_67 \def (lift1
 170 TMP_66 t) in (let TMP_68 \def (lift TMP_61 O TMP_67) in (eq T TMP_58
 171 TMP_68)))))))))))))) in (let TMP_159 \def (\lambda (H0: (eq bool (blt (trans
 172 hds0 i) d) true)).(let TMP_70 \def (trans hds0 i) in (let TMP_71 \def (S
 173 TMP_70) in (let TMP_72 \def (trans hds0 i) in (let TMP_73 \def (S TMP_72) in
 174 (let TMP_74 \def (minus d TMP_73) in (let TMP_75 \def (plus TMP_71 TMP_74) in
 175 (let TMP_91 \def (\lambda (n: nat).(let TMP_76 \def (trans hds0 i) in (let
 176 TMP_77 \def (S TMP_76) in (let TMP_78 \def (ptrans hds0 i) in (let TMP_79
 177 \def (lift1 TMP_78 t) in (let TMP_80 \def (lift TMP_77 O TMP_79) in (let
 178 TMP_81 \def (lift h n TMP_80) in (let TMP_82 \def (trans hds0 i) in (let
 179 TMP_83 \def (S TMP_82) in (let TMP_84 \def (trans hds0 i) in (let TMP_85 \def
 180 (S TMP_84) in (let TMP_86 \def (minus d TMP_85) in (let TMP_87 \def (ptrans
 181 hds0 i) in (let TMP_88 \def (PCons h TMP_86 TMP_87) in (let TMP_89 \def
 182 (lift1 TMP_88 t) in (let TMP_90 \def (lift TMP_83 O TMP_89) in (eq T TMP_81
 183 TMP_90))))))))))))))))) in (let TMP_92 \def (trans hds0 i) in (let TMP_93
 184 \def (S TMP_92) in (let TMP_94 \def (trans hds0 i) in (let TMP_95 \def (S
 185 TMP_94) in (let TMP_96 \def (minus d TMP_95) in (let TMP_97 \def (ptrans hds0
 186 i) in (let TMP_98 \def (lift1 TMP_97 t) in (let TMP_99 \def (lift h TMP_96
 187 TMP_98) in (let TMP_100 \def (lift TMP_93 O TMP_99) in (let TMP_110 \def
 188 (\lambda (t0: T).(let TMP_101 \def (trans hds0 i) in (let TMP_102 \def (S
 189 TMP_101) in (let TMP_103 \def (trans hds0 i) in (let TMP_104 \def (S TMP_103)
 190 in (let TMP_105 \def (minus d TMP_104) in (let TMP_106 \def (ptrans hds0 i)
 191 in (let TMP_107 \def (PCons h TMP_105 TMP_106) in (let TMP_108 \def (lift1
 192 TMP_107 t) in (let TMP_109 \def (lift TMP_102 O TMP_108) in (eq T t0
 193 TMP_109))))))))))) in (let TMP_111 \def (trans hds0 i) in (let TMP_112 \def
 194 (S TMP_111) in (let TMP_113 \def (trans hds0 i) in (let TMP_114 \def (S
 195 TMP_113) in (let TMP_115 \def (minus d TMP_114) in (let TMP_116 \def (ptrans
 196 hds0 i) in (let TMP_117 \def (PCons h TMP_115 TMP_116) in (let TMP_118 \def
 197 (lift1 TMP_117 t) in (let TMP_119 \def (lift TMP_112 O TMP_118) in (let
 198 TMP_120 \def (refl_equal T TMP_119) in (let TMP_121 \def (trans hds0 i) in
 199 (let TMP_122 \def (S TMP_121) in (let TMP_123 \def (trans hds0 i) in (let
 200 TMP_124 \def (S TMP_123) in (let TMP_125 \def (minus d TMP_124) in (let
 201 TMP_126 \def (plus TMP_122 TMP_125) in (let TMP_127 \def (trans hds0 i) in
 202 (let TMP_128 \def (S TMP_127) in (let TMP_129 \def (ptrans hds0 i) in (let
 203 TMP_130 \def (lift1 TMP_129 t) in (let TMP_131 \def (lift TMP_128 O TMP_130)
 204 in (let TMP_132 \def (lift h TMP_126 TMP_131) in (let TMP_133 \def (ptrans
 205 hds0 i) in (let TMP_134 \def (lift1 TMP_133 t) in (let TMP_135 \def (trans
 206 hds0 i) in (let TMP_136 \def (S TMP_135) in (let TMP_137 \def (trans hds0 i)
 207 in (let TMP_138 \def (S TMP_137) in (let TMP_139 \def (minus d TMP_138) in
 208 (let TMP_140 \def (trans hds0 i) in (let TMP_141 \def (S TMP_140) in (let
 209 TMP_142 \def (minus d TMP_141) in (let TMP_143 \def (le_O_n TMP_142) in (let
 210 TMP_144 \def (lift_d TMP_134 h TMP_136 TMP_139 O TMP_143) in (let TMP_145
 211 \def (eq_ind_r T TMP_100 TMP_110 TMP_120 TMP_132 TMP_144) in (let TMP_146
 212 \def (trans hds0 i) in (let TMP_147 \def (S TMP_146) in (let TMP_148 \def
 213 (trans hds0 i) in (let TMP_149 \def (S TMP_148) in (let TMP_150 \def (trans
 214 hds0 i) in (let TMP_151 \def (S TMP_150) in (let TMP_152 \def (trans hds0 i)
 215 in (let TMP_153 \def (trans hds0 i) in (let TMP_154 \def (blt_lt d TMP_153
 216 H0) in (let TMP_155 \def (lt_le_S TMP_152 d TMP_154) in (let TMP_156 \def
 217 (le_bge TMP_151 d TMP_155) in (let TMP_157 \def (bge_le TMP_149 d TMP_156) in
 218 (let TMP_158 \def (le_plus_minus TMP_147 d TMP_157) in (eq_ind_r nat TMP_75
 219 TMP_91 TMP_145 d
 220 TMP_158))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
 221 (let TMP_255 \def (\lambda (H0: (eq bool (blt (trans hds0 i) d) false)).(let
 222 TMP_160 \def (trans hds0 i) in (let TMP_161 \def (S TMP_160) in (let TMP_162
 223 \def (plus h TMP_161) in (let TMP_163 \def (ptrans hds0 i) in (let TMP_164
 224 \def (lift1 TMP_163 t) in (let TMP_165 \def (lift TMP_162 O TMP_164) in (let
 225 TMP_172 \def (\lambda (t0: T).(let TMP_166 \def (trans hds0 i) in (let
 226 TMP_167 \def (plus TMP_166 h) in (let TMP_168 \def (S TMP_167) in (let
 227 TMP_169 \def (ptrans hds0 i) in (let TMP_170 \def (lift1 TMP_169 t) in (let
 228 TMP_171 \def (lift TMP_168 O TMP_170) in (eq T t0 TMP_171)))))))) in (let
 229 TMP_173 \def (trans hds0 i) in (let TMP_174 \def (plus h TMP_173) in (let
 230 TMP_175 \def (S TMP_174) in (let TMP_185 \def (\lambda (n: nat).(let TMP_176
 231 \def (ptrans hds0 i) in (let TMP_177 \def (lift1 TMP_176 t) in (let TMP_178
 232 \def (lift n O TMP_177) in (let TMP_179 \def (trans hds0 i) in (let TMP_180
 233 \def (plus TMP_179 h) in (let TMP_181 \def (S TMP_180) in (let TMP_182 \def
 234 (ptrans hds0 i) in (let TMP_183 \def (lift1 TMP_182 t) in (let TMP_184 \def
 235 (lift TMP_181 O TMP_183) in (eq T TMP_178 TMP_184))))))))))) in (let TMP_186
 236 \def (trans hds0 i) in (let TMP_187 \def (plus TMP_186 h) in (let TMP_198
 237 \def (\lambda (n: nat).(let TMP_188 \def (S n) in (let TMP_189 \def (ptrans
 238 hds0 i) in (let TMP_190 \def (lift1 TMP_189 t) in (let TMP_191 \def (lift
 239 TMP_188 O TMP_190) in (let TMP_192 \def (trans hds0 i) in (let TMP_193 \def
 240 (plus TMP_192 h) in (let TMP_194 \def (S TMP_193) in (let TMP_195 \def
 241 (ptrans hds0 i) in (let TMP_196 \def (lift1 TMP_195 t) in (let TMP_197 \def
 242 (lift TMP_194 O TMP_196) in (eq T TMP_191 TMP_197)))))))))))) in (let TMP_199
 243 \def (trans hds0 i) in (let TMP_200 \def (plus TMP_199 h) in (let TMP_201
 244 \def (S TMP_200) in (let TMP_202 \def (ptrans hds0 i) in (let TMP_203 \def
 245 (lift1 TMP_202 t) in (let TMP_204 \def (lift TMP_201 O TMP_203) in (let
 246 TMP_205 \def (refl_equal T TMP_204) in (let TMP_206 \def (trans hds0 i) in
 247 (let TMP_207 \def (plus h TMP_206) in (let TMP_208 \def (trans hds0 i) in
 248 (let TMP_209 \def (plus_sym h TMP_208) in (let TMP_210 \def (eq_ind_r nat
 249 TMP_187 TMP_198 TMP_205 TMP_207 TMP_209) in (let TMP_211 \def (trans hds0 i)
 250 in (let TMP_212 \def (S TMP_211) in (let TMP_213 \def (plus h TMP_212) in
 251 (let TMP_214 \def (trans hds0 i) in (let TMP_215 \def (plus_n_Sm h TMP_214)
 252 in (let TMP_216 \def (eq_ind nat TMP_175 TMP_185 TMP_210 TMP_213 TMP_215) in
 253 (let TMP_217 \def (trans hds0 i) in (let TMP_218 \def (S TMP_217) in (let
 254 TMP_219 \def (ptrans hds0 i) in (let TMP_220 \def (lift1 TMP_219 t) in (let
 255 TMP_221 \def (lift TMP_218 O TMP_220) in (let TMP_222 \def (lift h d TMP_221)
 256 in (let TMP_223 \def (ptrans hds0 i) in (let TMP_224 \def (lift1 TMP_223 t)
 257 in (let TMP_225 \def (trans hds0 i) in (let TMP_226 \def (S TMP_225) in (let
 258 TMP_227 \def (trans hds0 i) in (let TMP_228 \def (plus O TMP_227) in (let
 259 TMP_229 \def (S TMP_228) in (let TMP_230 \def (\lambda (n: nat).(le d n)) in
 260 (let TMP_231 \def (trans hds0 i) in (let TMP_232 \def (plus TMP_231 O) in
 261 (let TMP_234 \def (\lambda (n: nat).(let TMP_233 \def (S n) in (le d
 262 TMP_233))) in (let TMP_235 \def (trans hds0 i) in (let TMP_236 \def (plus
 263 TMP_235 O) in (let TMP_237 \def (trans hds0 i) in (let TMP_238 \def (trans
 264 hds0 i) in (let TMP_239 \def (bge_le d TMP_238 H0) in (let TMP_240 \def
 265 (le_plus_trans d TMP_237 O TMP_239) in (let TMP_241 \def (le_S d TMP_236
 266 TMP_240) in (let TMP_242 \def (trans hds0 i) in (let TMP_243 \def (plus O
 267 TMP_242) in (let TMP_244 \def (trans hds0 i) in (let TMP_245 \def (plus_sym O
 268 TMP_244) in (let TMP_246 \def (eq_ind_r nat TMP_232 TMP_234 TMP_241 TMP_243
 269 TMP_245) in (let TMP_247 \def (trans hds0 i) in (let TMP_248 \def (S TMP_247)
 270 in (let TMP_249 \def (plus O TMP_248) in (let TMP_250 \def (trans hds0 i) in
 271 (let TMP_251 \def (plus_n_Sm O TMP_250) in (let TMP_252 \def (eq_ind nat
 272 TMP_229 TMP_230 TMP_246 TMP_249 TMP_251) in (let TMP_253 \def (le_O_n d) in
 273 (let TMP_254 \def (lift_free TMP_224 TMP_226 h O d TMP_252 TMP_253) in
 274 (eq_ind_r T TMP_165 TMP_172 TMP_216 TMP_222
 275 TMP_254)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 276  in (bool_ind TMP_69 TMP_159 TMP_255 x_x))))) in (let TMP_257 \def
 277 (xinduction bool TMP_35 TMP_52 TMP_256) in (let TMP_258 \def (S i) in (let
 278 TMP_259 \def (lift TMP_258 O t) in (let TMP_260 \def (lift1 hds0 TMP_259) in
 279 (let TMP_261 \def (H i t) in (eq_ind_r T TMP_17 TMP_33 TMP_257 TMP_260
 280 TMP_261)))))))))))))))))))))) in (PList_ind TMP_9 TMP_12 TMP_262 hds)))).
 281