-d n) \to (let TMP_1 \def (plus n h) in (let TMP_2 \def (lift h d t0) in (let
-TMP_3 \def (lift h d t3) in (subst0 TMP_1 t TMP_2 TMP_3)))))))))) in (let
-TMP_52 \def (\lambda (v: T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda
-(H0: (le d i0)).(let TMP_5 \def (plus i0 h) in (let TMP_6 \def (TLRef TMP_5)
-in (let TMP_11 \def (\lambda (t: T).(let TMP_7 \def (plus i0 h) in (let TMP_8
-\def (S i0) in (let TMP_9 \def (lift TMP_8 O v) in (let TMP_10 \def (lift h d
-TMP_9) in (subst0 TMP_7 v t TMP_10)))))) in (let TMP_12 \def (S i0) in (let
-TMP_13 \def (plus h TMP_12) in (let TMP_14 \def (lift TMP_13 O v) in (let
-TMP_18 \def (\lambda (t: T).(let TMP_15 \def (plus i0 h) in (let TMP_16 \def
-(plus i0 h) in (let TMP_17 \def (TLRef TMP_16) in (subst0 TMP_15 v TMP_17
-t))))) in (let TMP_19 \def (plus h i0) in (let TMP_20 \def (S TMP_19) in (let
-TMP_25 \def (\lambda (n: nat).(let TMP_21 \def (plus i0 h) in (let TMP_22
-\def (plus i0 h) in (let TMP_23 \def (TLRef TMP_22) in (let TMP_24 \def (lift
-n O v) in (subst0 TMP_21 v TMP_23 TMP_24)))))) in (let TMP_26 \def (plus h
-i0) in (let TMP_31 \def (\lambda (n: nat).(let TMP_27 \def (TLRef n) in (let
-TMP_28 \def (plus h i0) in (let TMP_29 \def (S TMP_28) in (let TMP_30 \def
-(lift TMP_29 O v) in (subst0 n v TMP_27 TMP_30)))))) in (let TMP_32 \def
-(plus h i0) in (let TMP_33 \def (subst0_lref v TMP_32) in (let TMP_34 \def
-(plus i0 h) in (let TMP_35 \def (plus_sym i0 h) in (let TMP_36 \def (eq_ind_r
-nat TMP_26 TMP_31 TMP_33 TMP_34 TMP_35) in (let TMP_37 \def (S i0) in (let
-TMP_38 \def (plus h TMP_37) in (let TMP_39 \def (plus_n_Sm h i0) in (let
-TMP_40 \def (eq_ind nat TMP_20 TMP_25 TMP_36 TMP_38 TMP_39) in (let TMP_41
-\def (S i0) in (let TMP_42 \def (lift TMP_41 O v) in (let TMP_43 \def (lift h
-d TMP_42) in (let TMP_44 \def (S i0) in (let TMP_45 \def (le_S d i0 H0) in
-(let TMP_46 \def (le_O_n d) in (let TMP_47 \def (lift_free v TMP_44 h O d
-TMP_45 TMP_46) in (let TMP_48 \def (eq_ind_r T TMP_14 TMP_18 TMP_40 TMP_43
-TMP_47) in (let TMP_49 \def (TLRef i0) in (let TMP_50 \def (lift h d TMP_49)
-in (let TMP_51 \def (lift_lref_ge i0 h d H0) in (eq_ind_r T TMP_6 TMP_11
-TMP_48 TMP_50 TMP_51))))))))))))))))))))))))))))))))))))) in (let TMP_85 \def
-(\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: nat).(\lambda
-(_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((le d i0) \to
-(subst0 (plus i0 h) v (lift h d u1) (lift h d u2)))))).(\lambda (t:
-T).(\lambda (k: K).(\lambda (d: nat).(\lambda (H2: (le d i0)).(let TMP_53
-\def (lift h d u1) in (let TMP_54 \def (s k d) in (let TMP_55 \def (lift h
-TMP_54 t) in (let TMP_56 \def (THead k TMP_53 TMP_55) in (let TMP_60 \def
-(\lambda (t0: T).(let TMP_57 \def (plus i0 h) in (let TMP_58 \def (THead k u2
-t) in (let TMP_59 \def (lift h d TMP_58) in (subst0 TMP_57 v t0 TMP_59)))))
-in (let TMP_61 \def (lift h d u2) in (let TMP_62 \def (s k d) in (let TMP_63
-\def (lift h TMP_62 t) in (let TMP_64 \def (THead k TMP_61 TMP_63) in (let
-TMP_70 \def (\lambda (t0: T).(let TMP_65 \def (plus i0 h) in (let TMP_66 \def
-(lift h d u1) in (let TMP_67 \def (s k d) in (let TMP_68 \def (lift h TMP_67
-t) in (let TMP_69 \def (THead k TMP_66 TMP_68) in (subst0 TMP_65 v TMP_69
-t0))))))) in (let TMP_71 \def (lift h d u2) in (let TMP_72 \def (lift h d u1)
-in (let TMP_73 \def (plus i0 h) in (let TMP_74 \def (H1 d H2) in (let TMP_75
-\def (s k d) in (let TMP_76 \def (lift h TMP_75 t) in (let TMP_77 \def
-(subst0_fst v TMP_71 TMP_72 TMP_73 TMP_74 TMP_76 k) in (let TMP_78 \def
-(THead k u2 t) in (let TMP_79 \def (lift h d TMP_78) in (let TMP_80 \def
-(lift_head k u2 t h d) in (let TMP_81 \def (eq_ind_r T TMP_64 TMP_70 TMP_77
-TMP_79 TMP_80) in (let TMP_82 \def (THead k u1 t) in (let TMP_83 \def (lift h
-d TMP_82) in (let TMP_84 \def (lift_head k u1 t h d) in (eq_ind_r T TMP_56
-TMP_60 TMP_81 TMP_83 TMP_84))))))))))))))))))))))))))))))))))) in (let
-TMP_129 \def (\lambda (k: K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3:
-T).(\lambda (i0: nat).(\lambda (_: (subst0 (s k i0) v t3 t0)).(\lambda (H1:
-((\forall (d: nat).((le d (s k i0)) \to (subst0 (plus (s k i0) h) v (lift h d
-t3) (lift h d t0)))))).(\lambda (u0: T).(\lambda (d: nat).(\lambda (H2: (le d
-i0)).(let TMP_86 \def (s k i0) in (let TMP_87 \def (plus TMP_86 h) in (let
-TMP_90 \def (\lambda (n: nat).(\forall (d0: nat).((le d0 (s k i0)) \to (let
-TMP_88 \def (lift h d0 t3) in (let TMP_89 \def (lift h d0 t0) in (subst0 n v
-TMP_88 TMP_89)))))) in (let TMP_91 \def (plus i0 h) in (let TMP_92 \def (s k
-TMP_91) in (let TMP_93 \def (s_plus k i0 h) in (let H3 \def (eq_ind_r nat
-TMP_87 TMP_90 H1 TMP_92 TMP_93) in (let TMP_94 \def (lift h d u0) in (let
-TMP_95 \def (s k d) in (let TMP_96 \def (lift h TMP_95 t3) in (let TMP_97
-\def (THead k TMP_94 TMP_96) in (let TMP_101 \def (\lambda (t: T).(let TMP_98
-\def (plus i0 h) in (let TMP_99 \def (THead k u0 t0) in (let TMP_100 \def
-(lift h d TMP_99) in (subst0 TMP_98 v t TMP_100))))) in (let TMP_102 \def
-(lift h d u0) in (let TMP_103 \def (s k d) in (let TMP_104 \def (lift h
-TMP_103 t0) in (let TMP_105 \def (THead k TMP_102 TMP_104) in (let TMP_111
-\def (\lambda (t: T).(let TMP_106 \def (plus i0 h) in (let TMP_107 \def (lift
-h d u0) in (let TMP_108 \def (s k d) in (let TMP_109 \def (lift h TMP_108 t3)
-in (let TMP_110 \def (THead k TMP_107 TMP_109) in (subst0 TMP_106 v TMP_110
-t))))))) in (let TMP_112 \def (s k d) in (let TMP_113 \def (lift h TMP_112
-t0) in (let TMP_114 \def (s k d) in (let TMP_115 \def (lift h TMP_114 t3) in
-(let TMP_116 \def (plus i0 h) in (let TMP_117 \def (s k d) in (let TMP_118
-\def (s_le k d i0 H2) in (let TMP_119 \def (H3 TMP_117 TMP_118) in (let
-TMP_120 \def (lift h d u0) in (let TMP_121 \def (subst0_snd k v TMP_113
-TMP_115 TMP_116 TMP_119 TMP_120) in (let TMP_122 \def (THead k u0 t0) in (let
-TMP_123 \def (lift h d TMP_122) in (let TMP_124 \def (lift_head k u0 t0 h d)
-in (let TMP_125 \def (eq_ind_r T TMP_105 TMP_111 TMP_121 TMP_123 TMP_124) in
-(let TMP_126 \def (THead k u0 t3) in (let TMP_127 \def (lift h d TMP_126) in
-(let TMP_128 \def (lift_head k u0 t3 h d) in (eq_ind_r T TMP_97 TMP_101
-TMP_125 TMP_127 TMP_128))))))))))))))))))))))))))))))))))))))))))))) in (let
-TMP_175 \def (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: