-u1)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (t1:
-T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c0 k t) t1 t2) \to (pc3
-(CHead c0 k t0) t1 t2)))))))) (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2:
-T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (k:
-K).(\lambda (H1: (pr2 (CHead c0 k t1) t0 t3)).(pc3_pr0_pr2_t t2 t1 H0 c0 t0
-t3 k H1))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
-(i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (t1:
-T).(\lambda (t2: T).(\lambda (H1: (pr0 t1 t2)).(\lambda (t: T).(\lambda (H2:
-(subst0 i u t2 t)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (k: K).(\lambda
-(H3: (pr2 (CHead c0 k t1) t0 t3)).(insert_eq C (CHead c0 k t1) (\lambda (c1:
-C).(pr2 c1 t0 t3)) (\lambda (_: C).(pc3 (CHead c0 k t) t0 t3)) (\lambda (y:
-C).(\lambda (H4: (pr2 y t0 t3)).(pr2_ind (\lambda (c1: C).(\lambda (t4:
-T).(\lambda (t5: T).((eq C c1 (CHead c0 k t1)) \to (pc3 (CHead c0 k t) t4
-t5))))) (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5: T).(\lambda (H5: (pr0
-t4 t5)).(\lambda (_: (eq C c1 (CHead c0 k t1))).(pc3_pr2_r (CHead c0 k t) t4
-t5 (pr2_free (CHead c0 k t) t4 t5 H5))))))) (\lambda (c1: C).(\lambda (d0:
-C).(\lambda (u0: T).(\lambda (i0: nat).(\lambda (H5: (getl i0 c1 (CHead d0
-(Bind Abbr) u0))).(\lambda (t4: T).(\lambda (t5: T).(\lambda (H6: (pr0 t4
-t5)).(\lambda (t6: T).(\lambda (H7: (subst0 i0 u0 t5 t6)).(\lambda (H8: (eq C
-c1 (CHead c0 k t1))).(let H9 \def (eq_ind C c1 (\lambda (c2: C).(getl i0 c2
-(CHead d0 (Bind Abbr) u0))) H5 (CHead c0 k t1) H8) in (nat_ind (\lambda (n:
-nat).((getl n (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to ((subst0 n u0 t5
-t6) \to (pc3 (CHead c0 k t) t4 t6)))) (\lambda (H10: (getl O (CHead c0 k t1)
-(CHead d0 (Bind Abbr) u0))).(\lambda (H11: (subst0 O u0 t5 t6)).(K_ind
-(\lambda (k0: K).((clear (CHead c0 k0 t1) (CHead d0 (Bind Abbr) u0)) \to (pc3
-(CHead c0 k0 t) t4 t6))) (\lambda (b: B).(\lambda (H12: (clear (CHead c0
-(Bind b) t1) (CHead d0 (Bind Abbr) u0))).(let H13 \def (f_equal C C (\lambda
-(e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d0
-| (CHead c2 _ _) \Rightarrow c2])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind
-b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H14
-\def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B)
-with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abbr])])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
-(clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H15 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow u0 | (CHead _ _ t7) \Rightarrow t7])) (CHead d0 (Bind
-Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr)
-u0) t1 H12)) in (\lambda (H16: (eq B Abbr b)).(\lambda (_: (eq C d0 c0)).(let
-H18 \def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t6)) H11 t1 H15) in
-(eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c0 (Bind b0) t) t4 t6)) (ex2_ind
-T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0 t6 t7)) (pc3
-(CHead c0 (Bind Abbr) t) t4 t6) (\lambda (x: T).(\lambda (H19: (subst0 O t2
-t5 x)).(\lambda (H20: (pr0 t6 x)).(ex2_ind T (\lambda (t7: T).(subst0 O t t5
-t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3 (CHead c0 (Bind
-Abbr) t) t4 t6) (\lambda (x0: T).(\lambda (H21: (subst0 O t t5 x0)).(\lambda
-(H22: (subst0 (S (plus i O)) u x x0)).(let H23 \def (f_equal nat nat S (plus
-i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in (let H24 \def (eq_ind nat
-(S (plus i O)) (\lambda (n: nat).(subst0 n u x x0)) H22 (S i) H23) in
-(pc3_pr2_u (CHead c0 (Bind Abbr) t) x0 t4 (pr2_delta (CHead c0 (Bind Abbr) t)
-c0 t O (getl_refl Abbr c0 t) t4 t5 H6 x0 H21) t6 (pc3_pr2_x (CHead c0 (Bind
-Abbr) t) x0 t6 (pr2_delta (CHead c0 (Bind Abbr) t) d u (S i) (getl_head (Bind
-Abbr) i c0 (CHead d (Bind Abbr) u) H0 t) t6 x H20 x0 H24))))))))
-(subst0_subst0_back t5 x t2 O H19 t u i H2))))) (pr0_subst0_fwd t1 t5 t6 O
-H18 t2 H1)) b H16))))) H14)) H13)))) (\lambda (f: F).(\lambda (H12: (clear
-(CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr) u0))).(clear_pc3_trans (CHead d0
-(Bind Abbr) u0) t4 t6 (pc3_pr2_r (CHead d0 (Bind Abbr) u0) t4 t6 (pr2_delta
-(CHead d0 (Bind Abbr) u0) d0 u0 O (getl_refl Abbr d0 u0) t4 t5 H6 t6 H11))
-(CHead c0 (Flat f) t) (clear_flat c0 (CHead d0 (Bind Abbr) u0)
-(clear_gen_flat f c0 (CHead d0 (Bind Abbr) u0) t1 H12) f t)))) k (getl_gen_O
-(CHead c0 k t1) (CHead d0 (Bind Abbr) u0) H10)))) (\lambda (i1: nat).(\lambda
-(_: (((getl i1 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to ((subst0 i1 u0
-t5 t6) \to (pc3 (CHead c0 k t) t4 t6))))).(\lambda (H10: (getl (S i1) (CHead
-c0 k t1) (CHead d0 (Bind Abbr) u0))).(\lambda (H11: (subst0 (S i1) u0 t5
-t6)).(K_ind (\lambda (k0: K).((getl (r k0 i1) c0 (CHead d0 (Bind Abbr) u0))
-\to (pc3 (CHead c0 k0 t) t4 t6))) (\lambda (b: B).(\lambda (H12: (getl (r
-(Bind b) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead c0 (Bind b) t)
-t4 t6 (pr2_delta (CHead c0 (Bind b) t) d0 u0 (S i1) (getl_head (Bind b) i1 c0
-(CHead d0 (Bind Abbr) u0) H12 t) t4 t5 H6 t6 H11)))) (\lambda (f: F).(\lambda
-(H12: (getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead
-c0 (Flat f) t) t4 t6 (pr2_cflat c0 t4 t6 (pr2_delta c0 d0 u0 (r (Flat f) i1)
-H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1
-i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1
-H)))).
-(* COMMENTS
-Initial nodes: 1671
-END *)
+u1)).(let TMP_2 \def (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
+T).(\forall (t1: T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c0 k t) t1
+t2) \to (let TMP_1 \def (CHead c0 k t0) in (pc3 TMP_1 t1 t2))))))))) in (let
+TMP_3 \def (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0:
+(pr0 t1 t2)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (k: K).(\lambda (H1:
+(pr2 (CHead c0 k t1) t0 t3)).(pc3_pr0_pr2_t t2 t1 H0 c0 t0 t3 k H1)))))))))
+in (let TMP_144 \def (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
+T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr)
+u))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H1: (pr0 t1 t2)).(\lambda
+(t: T).(\lambda (H2: (subst0 i u t2 t)).(\lambda (t0: T).(\lambda (t3:
+T).(\lambda (k: K).(\lambda (H3: (pr2 (CHead c0 k t1) t0 t3)).(let TMP_4 \def
+(CHead c0 k t1) in (let TMP_5 \def (\lambda (c1: C).(pr2 c1 t0 t3)) in (let
+TMP_7 \def (\lambda (_: C).(let TMP_6 \def (CHead c0 k t) in (pc3 TMP_6 t0
+t3))) in (let TMP_143 \def (\lambda (y: C).(\lambda (H4: (pr2 y t0 t3)).(let
+TMP_9 \def (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5: T).((eq C c1
+(CHead c0 k t1)) \to (let TMP_8 \def (CHead c0 k t) in (pc3 TMP_8 t4 t5))))))
+in (let TMP_13 \def (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5:
+T).(\lambda (H5: (pr0 t4 t5)).(\lambda (_: (eq C c1 (CHead c0 k t1))).(let
+TMP_10 \def (CHead c0 k t) in (let TMP_11 \def (CHead c0 k t) in (let TMP_12
+\def (pr2_free TMP_11 t4 t5 H5) in (pc3_pr2_r TMP_10 t4 t5 TMP_12))))))))) in
+(let TMP_142 \def (\lambda (c1: C).(\lambda (d0: C).(\lambda (u0: T).(\lambda
+(i0: nat).(\lambda (H5: (getl i0 c1 (CHead d0 (Bind Abbr) u0))).(\lambda (t4:
+T).(\lambda (t5: T).(\lambda (H6: (pr0 t4 t5)).(\lambda (t6: T).(\lambda (H7:
+(subst0 i0 u0 t5 t6)).(\lambda (H8: (eq C c1 (CHead c0 k t1))).(let TMP_16
+\def (\lambda (c2: C).(let TMP_14 \def (Bind Abbr) in (let TMP_15 \def (CHead
+d0 TMP_14 u0) in (getl i0 c2 TMP_15)))) in (let TMP_17 \def (CHead c0 k t1)
+in (let H9 \def (eq_ind C c1 TMP_16 H5 TMP_17 H8) in (let TMP_19 \def
+(\lambda (n: nat).((getl n (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to
+((subst0 n u0 t5 t6) \to (let TMP_18 \def (CHead c0 k t) in (pc3 TMP_18 t4
+t6))))) in (let TMP_117 \def (\lambda (H10: (getl O (CHead c0 k t1) (CHead d0
+(Bind Abbr) u0))).(\lambda (H11: (subst0 O u0 t5 t6)).(let TMP_21 \def
+(\lambda (k0: K).((clear (CHead c0 k0 t1) (CHead d0 (Bind Abbr) u0)) \to (let
+TMP_20 \def (CHead c0 k0 t) in (pc3 TMP_20 t4 t6)))) in (let TMP_94 \def
+(\lambda (b: B).(\lambda (H12: (clear (CHead c0 (Bind b) t1) (CHead d0 (Bind
+Abbr) u0))).(let TMP_22 \def (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d0 | (CHead c2 _ _) \Rightarrow c2])) in (let TMP_23 \def (Bind
+Abbr) in (let TMP_24 \def (CHead d0 TMP_23 u0) in (let TMP_25 \def (Bind b)
+in (let TMP_26 \def (CHead c0 TMP_25 t1) in (let TMP_27 \def (Bind Abbr) in
+(let TMP_28 \def (CHead d0 TMP_27 u0) in (let TMP_29 \def (clear_gen_bind b
+c0 TMP_28 t1 H12) in (let H13 \def (f_equal C C TMP_22 TMP_24 TMP_26 TMP_29)
+in (let TMP_30 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr
+| (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0) \Rightarrow b0 | (Flat
+_) \Rightarrow Abbr])])) in (let TMP_31 \def (Bind Abbr) in (let TMP_32 \def
+(CHead d0 TMP_31 u0) in (let TMP_33 \def (Bind b) in (let TMP_34 \def (CHead
+c0 TMP_33 t1) in (let TMP_35 \def (Bind Abbr) in (let TMP_36 \def (CHead d0
+TMP_35 u0) in (let TMP_37 \def (clear_gen_bind b c0 TMP_36 t1 H12) in (let
+H14 \def (f_equal C B TMP_30 TMP_32 TMP_34 TMP_37) in (let TMP_38 \def
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | (CHead _ _ t7)
+\Rightarrow t7])) in (let TMP_39 \def (Bind Abbr) in (let TMP_40 \def (CHead
+d0 TMP_39 u0) in (let TMP_41 \def (Bind b) in (let TMP_42 \def (CHead c0
+TMP_41 t1) in (let TMP_43 \def (Bind Abbr) in (let TMP_44 \def (CHead d0
+TMP_43 u0) in (let TMP_45 \def (clear_gen_bind b c0 TMP_44 t1 H12) in (let
+H15 \def (f_equal C T TMP_38 TMP_40 TMP_42 TMP_45) in (let TMP_92 \def
+(\lambda (H16: (eq B Abbr b)).(\lambda (_: (eq C d0 c0)).(let TMP_46 \def
+(\lambda (t7: T).(subst0 O t7 t5 t6)) in (let H18 \def (eq_ind T u0 TMP_46
+H11 t1 H15) in (let TMP_49 \def (\lambda (b0: B).(let TMP_47 \def (Bind b0)
+in (let TMP_48 \def (CHead c0 TMP_47 t) in (pc3 TMP_48 t4 t6)))) in (let
+TMP_50 \def (\lambda (t7: T).(subst0 O t2 t5 t7)) in (let TMP_51 \def
+(\lambda (t7: T).(pr0 t6 t7)) in (let TMP_52 \def (Bind Abbr) in (let TMP_53
+\def (CHead c0 TMP_52 t) in (let TMP_54 \def (pc3 TMP_53 t4 t6) in (let
+TMP_89 \def (\lambda (x: T).(\lambda (H19: (subst0 O t2 t5 x)).(\lambda (H20:
+(pr0 t6 x)).(let TMP_55 \def (\lambda (t7: T).(subst0 O t t5 t7)) in (let
+TMP_58 \def (\lambda (t7: T).(let TMP_56 \def (plus i O) in (let TMP_57 \def
+(S TMP_56) in (subst0 TMP_57 u x t7)))) in (let TMP_59 \def (Bind Abbr) in
+(let TMP_60 \def (CHead c0 TMP_59 t) in (let TMP_61 \def (pc3 TMP_60 t4 t6)
+in (let TMP_87 \def (\lambda (x0: T).(\lambda (H21: (subst0 O t t5
+x0)).(\lambda (H22: (subst0 (S (plus i O)) u x x0)).(let TMP_62 \def (plus i
+O) in (let TMP_63 \def (plus i O) in (let TMP_64 \def (plus_n_O i) in (let
+TMP_65 \def (sym_eq nat i TMP_63 TMP_64) in (let H23 \def (f_equal nat nat S
+TMP_62 i TMP_65) in (let TMP_66 \def (plus i O) in (let TMP_67 \def (S
+TMP_66) in (let TMP_68 \def (\lambda (n: nat).(subst0 n u x x0)) in (let
+TMP_69 \def (S i) in (let H24 \def (eq_ind nat TMP_67 TMP_68 H22 TMP_69 H23)
+in (let TMP_70 \def (Bind Abbr) in (let TMP_71 \def (CHead c0 TMP_70 t) in
+(let TMP_72 \def (Bind Abbr) in (let TMP_73 \def (CHead c0 TMP_72 t) in (let
+TMP_74 \def (getl_refl Abbr c0 t) in (let TMP_75 \def (pr2_delta TMP_73 c0 t
+O TMP_74 t4 t5 H6 x0 H21) in (let TMP_76 \def (Bind Abbr) in (let TMP_77 \def
+(CHead c0 TMP_76 t) in (let TMP_78 \def (Bind Abbr) in (let TMP_79 \def
+(CHead c0 TMP_78 t) in (let TMP_80 \def (S i) in (let TMP_81 \def (Bind Abbr)
+in (let TMP_82 \def (Bind Abbr) in (let TMP_83 \def (CHead d TMP_82 u) in
+(let TMP_84 \def (getl_head TMP_81 i c0 TMP_83 H0 t) in (let TMP_85 \def
+(pr2_delta TMP_79 d u TMP_80 TMP_84 t6 x H20 x0 H24) in (let TMP_86 \def
+(pc3_pr2_x TMP_77 x0 t6 TMP_85) in (pc3_pr2_u TMP_71 x0 t4 TMP_75 t6
+TMP_86))))))))))))))))))))))))))))))) in (let TMP_88 \def (subst0_subst0_back
+t5 x t2 O H19 t u i H2) in (ex2_ind T TMP_55 TMP_58 TMP_61 TMP_87
+TMP_88))))))))))) in (let TMP_90 \def (pr0_subst0_fwd t1 t5 t6 O H18 t2 H1)
+in (let TMP_91 \def (ex2_ind T TMP_50 TMP_51 TMP_54 TMP_89 TMP_90) in (eq_ind
+B Abbr TMP_49 TMP_91 b H16)))))))))))))) in (let TMP_93 \def (TMP_92 H14) in
+(TMP_93 H13)))))))))))))))))))))))))))))))) in (let TMP_112 \def (\lambda (f:
+F).(\lambda (H12: (clear (CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr)
+u0))).(let TMP_95 \def (Bind Abbr) in (let TMP_96 \def (CHead d0 TMP_95 u0)
+in (let TMP_97 \def (Bind Abbr) in (let TMP_98 \def (CHead d0 TMP_97 u0) in
+(let TMP_99 \def (Bind Abbr) in (let TMP_100 \def (CHead d0 TMP_99 u0) in
+(let TMP_101 \def (getl_refl Abbr d0 u0) in (let TMP_102 \def (pr2_delta
+TMP_100 d0 u0 O TMP_101 t4 t5 H6 t6 H11) in (let TMP_103 \def (pc3_pr2_r
+TMP_98 t4 t6 TMP_102) in (let TMP_104 \def (Flat f) in (let TMP_105 \def
+(CHead c0 TMP_104 t) in (let TMP_106 \def (Bind Abbr) in (let TMP_107 \def
+(CHead d0 TMP_106 u0) in (let TMP_108 \def (Bind Abbr) in (let TMP_109 \def
+(CHead d0 TMP_108 u0) in (let TMP_110 \def (clear_gen_flat f c0 TMP_109 t1
+H12) in (let TMP_111 \def (clear_flat c0 TMP_107 TMP_110 f t) in
+(clear_pc3_trans TMP_96 t4 t6 TMP_103 TMP_105 TMP_111)))))))))))))))))))) in
+(let TMP_113 \def (CHead c0 k t1) in (let TMP_114 \def (Bind Abbr) in (let
+TMP_115 \def (CHead d0 TMP_114 u0) in (let TMP_116 \def (getl_gen_O TMP_113
+TMP_115 H10) in (K_ind TMP_21 TMP_94 TMP_112 k TMP_116)))))))))) in (let
+TMP_141 \def (\lambda (i1: nat).(\lambda (_: (((getl i1 (CHead c0 k t1)
+(CHead d0 (Bind Abbr) u0)) \to ((subst0 i1 u0 t5 t6) \to (pc3 (CHead c0 k t)
+t4 t6))))).(\lambda (H10: (getl (S i1) (CHead c0 k t1) (CHead d0 (Bind Abbr)
+u0))).(\lambda (H11: (subst0 (S i1) u0 t5 t6)).(let TMP_119 \def (\lambda
+(k0: K).((getl (r k0 i1) c0 (CHead d0 (Bind Abbr) u0)) \to (let TMP_118 \def
+(CHead c0 k0 t) in (pc3 TMP_118 t4 t6)))) in (let TMP_130 \def (\lambda (b:
+B).(\lambda (H12: (getl (r (Bind b) i1) c0 (CHead d0 (Bind Abbr) u0))).(let
+TMP_120 \def (Bind b) in (let TMP_121 \def (CHead c0 TMP_120 t) in (let
+TMP_122 \def (Bind b) in (let TMP_123 \def (CHead c0 TMP_122 t) in (let
+TMP_124 \def (S i1) in (let TMP_125 \def (Bind b) in (let TMP_126 \def (Bind
+Abbr) in (let TMP_127 \def (CHead d0 TMP_126 u0) in (let TMP_128 \def
+(getl_head TMP_125 i1 c0 TMP_127 H12 t) in (let TMP_129 \def (pr2_delta
+TMP_123 d0 u0 TMP_124 TMP_128 t4 t5 H6 t6 H11) in (pc3_pr2_r TMP_121 t4 t6
+TMP_129))))))))))))) in (let TMP_137 \def (\lambda (f: F).(\lambda (H12:
+(getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0))).(let TMP_131 \def (Flat
+f) in (let TMP_132 \def (CHead c0 TMP_131 t) in (let TMP_133 \def (Flat f) in
+(let TMP_134 \def (r TMP_133 i1) in (let TMP_135 \def (pr2_delta c0 d0 u0
+TMP_134 H12 t4 t5 H6 t6 H11) in (let TMP_136 \def (pr2_cflat c0 t4 t6 TMP_135
+f t) in (pc3_pr2_r TMP_132 t4 t6 TMP_136))))))))) in (let TMP_138 \def (Bind
+Abbr) in (let TMP_139 \def (CHead d0 TMP_138 u0) in (let TMP_140 \def
+(getl_gen_S k c0 TMP_139 t1 i1 H10) in (K_ind TMP_119 TMP_130 TMP_137 k
+TMP_140))))))))))) in (nat_ind TMP_19 TMP_117 TMP_141 i0 H9
+H7)))))))))))))))))) in (pr2_ind TMP_9 TMP_13 TMP_142 y t0 t3 H4)))))) in
+(insert_eq C TMP_4 TMP_5 TMP_7 TMP_143 H3))))))))))))))))))) in (pr2_ind
+TMP_2 TMP_3 TMP_144 c u2 u1 H))))))).