matita/matita/contribs/lambdadelta/basic_1/subst/props.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1/subst/defs.ma".
  18
  19 include "basic_1/subst0/fwd.ma".
  20
  21 theorem subst_sort:
  22  \forall (v: T).(\forall (d: nat).(\forall (k: nat).(eq T (subst d v (TSort
  23 k)) (TSort k))))
  24 \def
  25  \lambda (_: T).(\lambda (_: nat).(\lambda (k: nat).(let TMP_1 \def (TSort k)
  26 in (refl_equal T TMP_1)))).
  27
  28 theorem subst_lref_lt:
  29  \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt i d) \to (eq T
  30 (subst d v (TLRef i)) (TLRef i)))))
  31 \def
  32  \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt i
  33 d)).(let TMP_5 \def (\lambda (b: bool).(let TMP_3 \def (match b with [true
  34 \Rightarrow (TLRef i) | false \Rightarrow (let TMP_1 \def (blt d i) in (match
  35 TMP_1 with [true \Rightarrow (let TMP_2 \def (pred i) in (TLRef TMP_2)) |
  36 false \Rightarrow (lift d O v)]))]) in (let TMP_4 \def (TLRef i) in (eq T
  37 TMP_3 TMP_4)))) in (let TMP_6 \def (TLRef i) in (let TMP_7 \def (refl_equal T
  38 TMP_6) in (let TMP_8 \def (blt i d) in (let TMP_9 \def (lt_blt d i H) in
  39 (eq_ind_r bool true TMP_5 TMP_7 TMP_8 TMP_9))))))))).
  40
  41 theorem subst_lref_eq:
  42  \forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v)))
  43 \def
  44  \lambda (v: T).(\lambda (i: nat).(let TMP_4 \def (\lambda (b: bool).(let
  45 TMP_2 \def (match b with [true \Rightarrow (TLRef i) | false \Rightarrow
  46 (match b with [true \Rightarrow (let TMP_1 \def (pred i) in (TLRef TMP_1)) |
  47 false \Rightarrow (lift i O v)])]) in (let TMP_3 \def (lift i O v) in (eq T
  48 TMP_2 TMP_3)))) in (let TMP_5 \def (lift i O v) in (let TMP_6 \def
  49 (refl_equal T TMP_5) in (let TMP_7 \def (blt i i) in (let TMP_8 \def (le_n i)
  50 in (let TMP_9 \def (le_bge i i TMP_8) in (eq_ind_r bool false TMP_4 TMP_6
  51 TMP_7 TMP_9)))))))).
  52
  53 theorem subst_lref_gt:
  54  \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt d i) \to (eq T
  55 (subst d v (TLRef i)) (TLRef (pred i))))))
  56 \def
  57  \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt d
  58 i)).(let TMP_6 \def (\lambda (b: bool).(let TMP_3 \def (match b with [true
  59 \Rightarrow (TLRef i) | false \Rightarrow (let TMP_1 \def (blt d i) in (match
  60 TMP_1 with [true \Rightarrow (let TMP_2 \def (pred i) in (TLRef TMP_2)) |
  61 false \Rightarrow (lift d O v)]))]) in (let TMP_4 \def (pred i) in (let TMP_5
  62 \def (TLRef TMP_4) in (eq T TMP_3 TMP_5))))) in (let TMP_11 \def (\lambda (b:
  63 bool).(let TMP_8 \def (match b with [true \Rightarrow (let TMP_7 \def (pred
  64 i) in (TLRef TMP_7)) | false \Rightarrow (lift d O v)]) in (let TMP_9 \def
  65 (pred i) in (let TMP_10 \def (TLRef TMP_9) in (eq T TMP_8 TMP_10))))) in (let
  66 TMP_12 \def (pred i) in (let TMP_13 \def (TLRef TMP_12) in (let TMP_14 \def
  67 (refl_equal T TMP_13) in (let TMP_15 \def (blt d i) in (let TMP_16 \def
  68 (lt_blt i d H) in (let TMP_17 \def (eq_ind_r bool true TMP_11 TMP_14 TMP_15
  69 TMP_16) in (let TMP_18 \def (blt i d) in (let TMP_19 \def (lt_le_weak d i H)
  70 in (let TMP_20 \def (le_bge d i TMP_19) in (eq_ind_r bool false TMP_6 TMP_17
  71 TMP_18 TMP_20))))))))))))))).
  72
  73 theorem subst_head:
  74  \forall (k: K).(\forall (w: T).(\forall (u: T).(\forall (t: T).(\forall (d:
  75 nat).(eq T (subst d w (THead k u t)) (THead k (subst d w u) (subst (s k d) w
  76 t)))))))
  77 \def
  78  \lambda (k: K).(\lambda (w: T).(\lambda (u: T).(\lambda (t: T).(\lambda (d:
  79 nat).(let TMP_1 \def (subst d w u) in (let TMP_2 \def (s k d) in (let TMP_3
  80 \def (subst TMP_2 w t) in (let TMP_4 \def (THead k TMP_1 TMP_3) in
  81 (refl_equal T TMP_4))))))))).
  82
  83 theorem subst_lift_SO:
  84  \forall (v: T).(\forall (t: T).(\forall (d: nat).(eq T (subst d v (lift (S
  85 O) d t)) t)))
  86 \def
  87  \lambda (v: T).(\lambda (t: T).(let TMP_4 \def (\lambda (t0: T).(\forall (d:
  88 nat).(let TMP_1 \def (S O) in (let TMP_2 \def (lift TMP_1 d t0) in (let TMP_3
  89 \def (subst d v TMP_2) in (eq T TMP_3 t0)))))) in (let TMP_23 \def (\lambda
  90 (n: nat).(\lambda (d: nat).(let TMP_5 \def (TSort n) in (let TMP_8 \def
  91 (\lambda (t0: T).(let TMP_6 \def (subst d v t0) in (let TMP_7 \def (TSort n)
  92 in (eq T TMP_6 TMP_7)))) in (let TMP_9 \def (TSort n) in (let TMP_11 \def
  93 (\lambda (t0: T).(let TMP_10 \def (TSort n) in (eq T t0 TMP_10))) in (let
  94 TMP_12 \def (TSort n) in (let TMP_13 \def (refl_equal T TMP_12) in (let
  95 TMP_14 \def (TSort n) in (let TMP_15 \def (subst d v TMP_14) in (let TMP_16
  96 \def (subst_sort v d n) in (let TMP_17 \def (eq_ind_r T TMP_9 TMP_11 TMP_13
  97 TMP_15 TMP_16) in (let TMP_18 \def (S O) in (let TMP_19 \def (TSort n) in
  98 (let TMP_20 \def (lift TMP_18 d TMP_19) in (let TMP_21 \def (S O) in (let
  99 TMP_22 \def (lift_sort n TMP_21 d) in (eq_ind_r T TMP_5 TMP_8 TMP_17 TMP_20
 100 TMP_22)))))))))))))))))) in (let TMP_103 \def (\lambda (n: nat).(\lambda (d:
 101 nat).(let TMP_24 \def (S O) in (let TMP_25 \def (TLRef n) in (let TMP_26 \def
 102 (lift TMP_24 d TMP_25) in (let TMP_27 \def (subst d v TMP_26) in (let TMP_28
 103 \def (TLRef n) in (let TMP_29 \def (eq T TMP_27 TMP_28) in (let TMP_48 \def
 104 (\lambda (H: (lt n d)).(let TMP_30 \def (TLRef n) in (let TMP_33 \def
 105 (\lambda (t0: T).(let TMP_31 \def (subst d v t0) in (let TMP_32 \def (TLRef
 106 n) in (eq T TMP_31 TMP_32)))) in (let TMP_34 \def (TLRef n) in (let TMP_36
 107 \def (\lambda (t0: T).(let TMP_35 \def (TLRef n) in (eq T t0 TMP_35))) in
 108 (let TMP_37 \def (TLRef n) in (let TMP_38 \def (refl_equal T TMP_37) in (let
 109 TMP_39 \def (TLRef n) in (let TMP_40 \def (subst d v TMP_39) in (let TMP_41
 110 \def (subst_lref_lt v d n H) in (let TMP_42 \def (eq_ind_r T TMP_34 TMP_36
 111 TMP_38 TMP_40 TMP_41) in (let TMP_43 \def (S O) in (let TMP_44 \def (TLRef n)
 112 in (let TMP_45 \def (lift TMP_43 d TMP_44) in (let TMP_46 \def (S O) in (let
 113 TMP_47 \def (lift_lref_lt n TMP_46 d H) in (eq_ind_r T TMP_30 TMP_33 TMP_42
 114 TMP_45 TMP_47))))))))))))))))) in (let TMP_102 \def (\lambda (H: (le d
 115 n)).(let TMP_49 \def (S O) in (let TMP_50 \def (plus n TMP_49) in (let TMP_51
 116 \def (TLRef TMP_50) in (let TMP_54 \def (\lambda (t0: T).(let TMP_52 \def
 117 (subst d v t0) in (let TMP_53 \def (TLRef n) in (eq T TMP_52 TMP_53)))) in
 118 (let TMP_55 \def (plus n O) in (let TMP_56 \def (S TMP_55) in (let TMP_60
 119 \def (\lambda (n0: nat).(let TMP_57 \def (TLRef n0) in (let TMP_58 \def
 120 (subst d v TMP_57) in (let TMP_59 \def (TLRef n) in (eq T TMP_58 TMP_59)))))
 121 in (let TMP_61 \def (plus n O) in (let TMP_62 \def (S TMP_61) in (let TMP_63
 122 \def (pred TMP_62) in (let TMP_64 \def (TLRef TMP_63) in (let TMP_66 \def
 123 (\lambda (t0: T).(let TMP_65 \def (TLRef n) in (eq T t0 TMP_65))) in (let
 124 TMP_67 \def (plus n O) in (let TMP_70 \def (\lambda (n0: nat).(let TMP_68
 125 \def (TLRef n0) in (let TMP_69 \def (TLRef n) in (eq T TMP_68 TMP_69)))) in
 126 (let TMP_71 \def (plus n O) in (let TMP_72 \def (plus n O) in (let TMP_73
 127 \def (plus_n_O n) in (let TMP_74 \def (sym_eq nat n TMP_72 TMP_73) in (let
 128 TMP_75 \def (f_equal nat T TLRef TMP_71 n TMP_74) in (let TMP_76 \def (plus n
 129 O) in (let TMP_77 \def (S TMP_76) in (let TMP_78 \def (pred TMP_77) in (let
 130 TMP_79 \def (plus n O) in (let TMP_80 \def (pred_Sn TMP_79) in (let TMP_81
 131 \def (eq_ind nat TMP_67 TMP_70 TMP_75 TMP_78 TMP_80) in (let TMP_82 \def
 132 (plus n O) in (let TMP_83 \def (S TMP_82) in (let TMP_84 \def (TLRef TMP_83)
 133 in (let TMP_85 \def (subst d v TMP_84) in (let TMP_86 \def (plus n O) in (let
 134 TMP_87 \def (S TMP_86) in (let TMP_88 \def (plus n O) in (let TMP_89 \def
 135 (le_plus_trans d n O H) in (let TMP_90 \def (le_n_S d TMP_88 TMP_89) in (let
 136 TMP_91 \def (subst_lref_gt v d TMP_87 TMP_90) in (let TMP_92 \def (eq_ind_r T
 137 TMP_64 TMP_66 TMP_81 TMP_85 TMP_91) in (let TMP_93 \def (S O) in (let TMP_94
 138 \def (plus n TMP_93) in (let TMP_95 \def (plus_n_Sm n O) in (let TMP_96 \def
 139 (eq_ind nat TMP_56 TMP_60 TMP_92 TMP_94 TMP_95) in (let TMP_97 \def (S O) in
 140 (let TMP_98 \def (TLRef n) in (let TMP_99 \def (lift TMP_97 d TMP_98) in (let
 141 TMP_100 \def (S O) in (let TMP_101 \def (lift_lref_ge n TMP_100 d H) in
 142 (eq_ind_r T TMP_51 TMP_54 TMP_96 TMP_99
 143 TMP_101))))))))))))))))))))))))))))))))))))))))))))))) in (lt_le_e n d TMP_29
 144 TMP_48 TMP_102))))))))))) in (let TMP_178 \def (\lambda (k: K).(\lambda (t0:
 145 T).(\lambda (H: ((\forall (d: nat).(eq T (subst d v (lift (S O) d t0))
 146 t0)))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(eq T (subst d v
 147 (lift (S O) d t1)) t1)))).(\lambda (d: nat).(let TMP_104 \def (S O) in (let
 148 TMP_105 \def (lift TMP_104 d t0) in (let TMP_106 \def (S O) in (let TMP_107
 149 \def (s k d) in (let TMP_108 \def (lift TMP_106 TMP_107 t1) in (let TMP_109
 150 \def (THead k TMP_105 TMP_108) in (let TMP_112 \def (\lambda (t2: T).(let
 151 TMP_110 \def (subst d v t2) in (let TMP_111 \def (THead k t0 t1) in (eq T
 152 TMP_110 TMP_111)))) in (let TMP_113 \def (S O) in (let TMP_114 \def (lift
 153 TMP_113 d t0) in (let TMP_115 \def (subst d v TMP_114) in (let TMP_116 \def
 154 (s k d) in (let TMP_117 \def (S O) in (let TMP_118 \def (s k d) in (let
 155 TMP_119 \def (lift TMP_117 TMP_118 t1) in (let TMP_120 \def (subst TMP_116 v
 156 TMP_119) in (let TMP_121 \def (THead k TMP_115 TMP_120) in (let TMP_123 \def
 157 (\lambda (t2: T).(let TMP_122 \def (THead k t0 t1) in (eq T t2 TMP_122))) in
 158 (let TMP_124 \def (THead k t0 t1) in (let TMP_125 \def (S O) in (let TMP_126
 159 \def (lift TMP_125 d t0) in (let TMP_127 \def (subst d v TMP_126) in (let
 160 TMP_128 \def (s k d) in (let TMP_129 \def (S O) in (let TMP_130 \def (s k d)
 161 in (let TMP_131 \def (lift TMP_129 TMP_130 t1) in (let TMP_132 \def (subst
 162 TMP_128 v TMP_131) in (let TMP_133 \def (THead k TMP_127 TMP_132) in (let
 163 TMP_134 \def (S O) in (let TMP_135 \def (lift TMP_134 d t0) in (let TMP_136
 164 \def (subst d v TMP_135) in (let TMP_137 \def (s k d) in (let TMP_138 \def (S
 165 O) in (let TMP_139 \def (s k d) in (let TMP_140 \def (lift TMP_138 TMP_139
 166 t1) in (let TMP_141 \def (subst TMP_137 v TMP_140) in (let TMP_142 \def
 167 (THead k TMP_136 TMP_141) in (let TMP_143 \def (THead k t0 t1) in (let
 168 TMP_144 \def (S O) in (let TMP_145 \def (lift TMP_144 d t0) in (let TMP_146
 169 \def (subst d v TMP_145) in (let TMP_147 \def (s k d) in (let TMP_148 \def (S
 170 O) in (let TMP_149 \def (s k d) in (let TMP_150 \def (lift TMP_148 TMP_149
 171 t1) in (let TMP_151 \def (subst TMP_147 v TMP_150) in (let TMP_152 \def
 172 (refl_equal K k) in (let TMP_153 \def (H d) in (let TMP_154 \def (s k d) in
 173 (let TMP_155 \def (H0 TMP_154) in (let TMP_156 \def (f_equal3 K T T T THead k
 174 k TMP_146 t0 TMP_151 t1 TMP_152 TMP_153 TMP_155) in (let TMP_157 \def (sym_eq
 175 T TMP_142 TMP_143 TMP_156) in (let TMP_158 \def (sym_eq T TMP_124 TMP_133
 176 TMP_157) in (let TMP_159 \def (S O) in (let TMP_160 \def (lift TMP_159 d t0)
 177 in (let TMP_161 \def (S O) in (let TMP_162 \def (s k d) in (let TMP_163 \def
 178 (lift TMP_161 TMP_162 t1) in (let TMP_164 \def (THead k TMP_160 TMP_163) in
 179 (let TMP_165 \def (subst d v TMP_164) in (let TMP_166 \def (S O) in (let
 180 TMP_167 \def (lift TMP_166 d t0) in (let TMP_168 \def (S O) in (let TMP_169
 181 \def (s k d) in (let TMP_170 \def (lift TMP_168 TMP_169 t1) in (let TMP_171
 182 \def (subst_head k v TMP_167 TMP_170 d) in (let TMP_172 \def (eq_ind_r T
 183 TMP_121 TMP_123 TMP_158 TMP_165 TMP_171) in (let TMP_173 \def (S O) in (let
 184 TMP_174 \def (THead k t0 t1) in (let TMP_175 \def (lift TMP_173 d TMP_174) in
 185 (let TMP_176 \def (S O) in (let TMP_177 \def (lift_head k t0 t1 TMP_176 d) in
 186 (eq_ind_r T TMP_109 TMP_112 TMP_172 TMP_175
 187 TMP_177)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 188 ))))))) in (T_ind TMP_4 TMP_23 TMP_103 TMP_178 t)))))).
 189
 190 theorem subst_subst0:
 191  \forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall (d: nat).((subst0
 192 d v t1 t2) \to (eq T (subst d v t1) (subst d v t2))))))
 193 \def
 194  \lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (d: nat).(\lambda
 195 (H: (subst0 d v t1 t2)).(let TMP_3 \def (\lambda (n: nat).(\lambda (t:
 196 T).(\lambda (t0: T).(\lambda (t3: T).(let TMP_1 \def (subst n t t0) in (let
 197 TMP_2 \def (subst n t t3) in (eq T TMP_1 TMP_2))))))) in (let TMP_49 \def
 198 (\lambda (v0: T).(\lambda (i: nat).(let TMP_4 \def (lift i O v0) in (let
 199 TMP_8 \def (\lambda (t: T).(let TMP_5 \def (S i) in (let TMP_6 \def (lift
 200 TMP_5 O v0) in (let TMP_7 \def (subst i v0 TMP_6) in (eq T t TMP_7))))) in
 201 (let TMP_9 \def (S O) in (let TMP_10 \def (plus TMP_9 i) in (let TMP_14 \def
 202 (\lambda (n: nat).(let TMP_11 \def (lift i O v0) in (let TMP_12 \def (lift n
 203 O v0) in (let TMP_13 \def (subst i v0 TMP_12) in (eq T TMP_11 TMP_13))))) in
 204 (let TMP_15 \def (S O) in (let TMP_16 \def (lift i O v0) in (let TMP_17 \def
 205 (lift TMP_15 i TMP_16) in (let TMP_20 \def (\lambda (t: T).(let TMP_18 \def
 206 (lift i O v0) in (let TMP_19 \def (subst i v0 t) in (eq T TMP_18 TMP_19))))
 207 in (let TMP_21 \def (lift i O v0) in (let TMP_23 \def (\lambda (t: T).(let
 208 TMP_22 \def (lift i O v0) in (eq T TMP_22 t))) in (let TMP_24 \def (lift i O
 209 v0) in (let TMP_25 \def (refl_equal T TMP_24) in (let TMP_26 \def (S O) in
 210 (let TMP_27 \def (lift i O v0) in (let TMP_28 \def (lift TMP_26 i TMP_27) in
 211 (let TMP_29 \def (subst i v0 TMP_28) in (let TMP_30 \def (lift i O v0) in
 212 (let TMP_31 \def (subst_lift_SO v0 TMP_30 i) in (let TMP_32 \def (eq_ind_r T
 213 TMP_21 TMP_23 TMP_25 TMP_29 TMP_31) in (let TMP_33 \def (S O) in (let TMP_34
 214 \def (plus TMP_33 i) in (let TMP_35 \def (lift TMP_34 O v0) in (let TMP_36
 215 \def (S O) in (let TMP_37 \def (plus O i) in (let TMP_38 \def (le_n TMP_37)
 216 in (let TMP_39 \def (le_O_n i) in (let TMP_40 \def (lift_free v0 i TMP_36 O i
 217 TMP_38 TMP_39) in (let TMP_41 \def (eq_ind T TMP_17 TMP_20 TMP_32 TMP_35
 218 TMP_40) in (let TMP_42 \def (S i) in (let TMP_43 \def (S i) in (let TMP_44
 219 \def (refl_equal nat TMP_43) in (let TMP_45 \def (eq_ind nat TMP_10 TMP_14
 220 TMP_41 TMP_42 TMP_44) in (let TMP_46 \def (TLRef i) in (let TMP_47 \def
 221 (subst i v0 TMP_46) in (let TMP_48 \def (subst_lref_eq v0 i) in (eq_ind_r T
 222 TMP_4 TMP_8 TMP_45 TMP_47 TMP_48))))))))))))))))))))))))))))))))))))))) in
 223 (let TMP_89 \def (\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda
 224 (i: nat).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0
 225 u1) (subst i v0 u2))).(\lambda (t: T).(\lambda (k: K).(let TMP_50 \def (subst
 226 i v0 u1) in (let TMP_51 \def (s k i) in (let TMP_52 \def (subst TMP_51 v0 t)
 227 in (let TMP_53 \def (THead k TMP_50 TMP_52) in (let TMP_56 \def (\lambda (t0:
 228 T).(let TMP_54 \def (THead k u2 t) in (let TMP_55 \def (subst i v0 TMP_54) in
 229 (eq T t0 TMP_55)))) in (let TMP_57 \def (subst i v0 u2) in (let TMP_58 \def
 230 (s k i) in (let TMP_59 \def (subst TMP_58 v0 t) in (let TMP_60 \def (THead k
 231 TMP_57 TMP_59) in (let TMP_65 \def (\lambda (t0: T).(let TMP_61 \def (subst i
 232 v0 u1) in (let TMP_62 \def (s k i) in (let TMP_63 \def (subst TMP_62 v0 t) in
 233 (let TMP_64 \def (THead k TMP_61 TMP_63) in (eq T TMP_64 t0)))))) in (let
 234 TMP_66 \def (subst i v0 u2) in (let TMP_74 \def (\lambda (t0: T).(let TMP_67
 235 \def (s k i) in (let TMP_68 \def (subst TMP_67 v0 t) in (let TMP_69 \def
 236 (THead k t0 TMP_68) in (let TMP_70 \def (subst i v0 u2) in (let TMP_71 \def
 237 (s k i) in (let TMP_72 \def (subst TMP_71 v0 t) in (let TMP_73 \def (THead k
 238 TMP_70 TMP_72) in (eq T TMP_69 TMP_73))))))))) in (let TMP_75 \def (subst i
 239 v0 u2) in (let TMP_76 \def (s k i) in (let TMP_77 \def (subst TMP_76 v0 t) in
 240 (let TMP_78 \def (THead k TMP_75 TMP_77) in (let TMP_79 \def (refl_equal T
 241 TMP_78) in (let TMP_80 \def (subst i v0 u1) in (let TMP_81 \def (eq_ind_r T
 242 TMP_66 TMP_74 TMP_79 TMP_80 H1) in (let TMP_82 \def (THead k u2 t) in (let
 243 TMP_83 \def (subst i v0 TMP_82) in (let TMP_84 \def (subst_head k v0 u2 t i)
 244 in (let TMP_85 \def (eq_ind_r T TMP_60 TMP_65 TMP_81 TMP_83 TMP_84) in (let
 245 TMP_86 \def (THead k u1 t) in (let TMP_87 \def (subst i v0 TMP_86) in (let
 246 TMP_88 \def (subst_head k v0 u1 t i) in (eq_ind_r T TMP_53 TMP_56 TMP_85
 247 TMP_87 TMP_88))))))))))))))))))))))))))))))))))) in (let TMP_130 \def
 248 (\lambda (k: K).(\lambda (v0: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda
 249 (i: nat).(\lambda (_: (subst0 (s k i) v0 t4 t3)).(\lambda (H1: (eq T (subst
 250 (s k i) v0 t4) (subst (s k i) v0 t3))).(\lambda (u: T).(let TMP_90 \def
 251 (subst i v0 u) in (let TMP_91 \def (s k i) in (let TMP_92 \def (subst TMP_91
 252 v0 t4) in (let TMP_93 \def (THead k TMP_90 TMP_92) in (let TMP_96 \def
 253 (\lambda (t: T).(let TMP_94 \def (THead k u t3) in (let TMP_95 \def (subst i
 254 v0 TMP_94) in (eq T t TMP_95)))) in (let TMP_97 \def (subst i v0 u) in (let
 255 TMP_98 \def (s k i) in (let TMP_99 \def (subst TMP_98 v0 t3) in (let TMP_100
 256 \def (THead k TMP_97 TMP_99) in (let TMP_105 \def (\lambda (t: T).(let
 257 TMP_101 \def (subst i v0 u) in (let TMP_102 \def (s k i) in (let TMP_103 \def
 258 (subst TMP_102 v0 t4) in (let TMP_104 \def (THead k TMP_101 TMP_103) in (eq T
 259 TMP_104 t)))))) in (let TMP_106 \def (s k i) in (let TMP_107 \def (subst
 260 TMP_106 v0 t3) in (let TMP_114 \def (\lambda (t: T).(let TMP_108 \def (subst
 261 i v0 u) in (let TMP_109 \def (THead k TMP_108 t) in (let TMP_110 \def (subst
 262 i v0 u) in (let TMP_111 \def (s k i) in (let TMP_112 \def (subst TMP_111 v0
 263 t3) in (let TMP_113 \def (THead k TMP_110 TMP_112) in (eq T TMP_109
 264 TMP_113)))))))) in (let TMP_115 \def (subst i v0 u) in (let TMP_116 \def (s k
 265 i) in (let TMP_117 \def (subst TMP_116 v0 t3) in (let TMP_118 \def (THead k
 266 TMP_115 TMP_117) in (let TMP_119 \def (refl_equal T TMP_118) in (let TMP_120
 267 \def (s k i) in (let TMP_121 \def (subst TMP_120 v0 t4) in (let TMP_122 \def
 268 (eq_ind_r T TMP_107 TMP_114 TMP_119 TMP_121 H1) in (let TMP_123 \def (THead k
 269 u t3) in (let TMP_124 \def (subst i v0 TMP_123) in (let TMP_125 \def
 270 (subst_head k v0 u t3 i) in (let TMP_126 \def (eq_ind_r T TMP_100 TMP_105
 271 TMP_122 TMP_124 TMP_125) in (let TMP_127 \def (THead k u t4) in (let TMP_128
 272 \def (subst i v0 TMP_127) in (let TMP_129 \def (subst_head k v0 u t4 i) in
 273 (eq_ind_r T TMP_93 TMP_96 TMP_126 TMP_128
 274 TMP_129))))))))))))))))))))))))))))))))))))) in (let TMP_182 \def (\lambda
 275 (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (_:
 276 (subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0 u1) (subst i v0
 277 u2))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (subst0
 278 (s k i) v0 t3 t4)).(\lambda (H3: (eq T (subst (s k i) v0 t3) (subst (s k i)
 279 v0 t4))).(let TMP_131 \def (subst i v0 u1) in (let TMP_132 \def (s k i) in
 280 (let TMP_133 \def (subst TMP_132 v0 t3) in (let TMP_134 \def (THead k TMP_131
 281 TMP_133) in (let TMP_137 \def (\lambda (t: T).(let TMP_135 \def (THead k u2
 282 t4) in (let TMP_136 \def (subst i v0 TMP_135) in (eq T t TMP_136)))) in (let
 283 TMP_138 \def (subst i v0 u2) in (let TMP_139 \def (s k i) in (let TMP_140
 284 \def (subst TMP_139 v0 t4) in (let TMP_141 \def (THead k TMP_138 TMP_140) in
 285 (let TMP_146 \def (\lambda (t: T).(let TMP_142 \def (subst i v0 u1) in (let
 286 TMP_143 \def (s k i) in (let TMP_144 \def (subst TMP_143 v0 t3) in (let
 287 TMP_145 \def (THead k TMP_142 TMP_144) in (eq T TMP_145 t)))))) in (let
 288 TMP_147 \def (subst i v0 u2) in (let TMP_155 \def (\lambda (t: T).(let
 289 TMP_148 \def (s k i) in (let TMP_149 \def (subst TMP_148 v0 t3) in (let
 290 TMP_150 \def (THead k t TMP_149) in (let TMP_151 \def (subst i v0 u2) in (let
 291 TMP_152 \def (s k i) in (let TMP_153 \def (subst TMP_152 v0 t4) in (let
 292 TMP_154 \def (THead k TMP_151 TMP_153) in (eq T TMP_150 TMP_154))))))))) in
 293 (let TMP_156 \def (s k i) in (let TMP_157 \def (subst TMP_156 v0 t4) in (let
 294 TMP_164 \def (\lambda (t: T).(let TMP_158 \def (subst i v0 u2) in (let
 295 TMP_159 \def (THead k TMP_158 t) in (let TMP_160 \def (subst i v0 u2) in (let
 296 TMP_161 \def (s k i) in (let TMP_162 \def (subst TMP_161 v0 t4) in (let
 297 TMP_163 \def (THead k TMP_160 TMP_162) in (eq T TMP_159 TMP_163)))))))) in
 298 (let TMP_165 \def (subst i v0 u2) in (let TMP_166 \def (s k i) in (let
 299 TMP_167 \def (subst TMP_166 v0 t4) in (let TMP_168 \def (THead k TMP_165
 300 TMP_167) in (let TMP_169 \def (refl_equal T TMP_168) in (let TMP_170 \def (s
 301 k i) in (let TMP_171 \def (subst TMP_170 v0 t3) in (let TMP_172 \def
 302 (eq_ind_r T TMP_157 TMP_164 TMP_169 TMP_171 H3) in (let TMP_173 \def (subst i
 303 v0 u1) in (let TMP_174 \def (eq_ind_r T TMP_147 TMP_155 TMP_172 TMP_173 H1)
 304 in (let TMP_175 \def (THead k u2 t4) in (let TMP_176 \def (subst i v0
 305 TMP_175) in (let TMP_177 \def (subst_head k v0 u2 t4 i) in (let TMP_178 \def
 306 (eq_ind_r T TMP_141 TMP_146 TMP_174 TMP_176 TMP_177) in (let TMP_179 \def
 307 (THead k u1 t3) in (let TMP_180 \def (subst i v0 TMP_179) in (let TMP_181
 308 \def (subst_head k v0 u1 t3 i) in (eq_ind_r T TMP_134 TMP_137 TMP_178 TMP_180
 309 TMP_181)))))))))))))))))))))))))))))))))))))))))))) in (subst0_ind TMP_3
 310 TMP_49 TMP_89 TMP_130 TMP_182 d v t1 t2 H)))))))))).
 311