-t2)).(let TMP_1 \def (\lambda (t: T).(\lambda (t0: T).(\forall (t3:
-T).((pc3_left c t0 t3) \to (pc3_left c t t3))))) in (let TMP_2 \def (\lambda
-(t: T).(\lambda (t3: T).(\lambda (H0: (pc3_left c t t3)).H0))) in (let TMP_4
-\def (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c t0 t3)).(\lambda
-(t4: T).(\lambda (_: (pc3_left c t3 t4)).(\lambda (H2: ((\forall (t5:
-T).((pc3_left c t4 t5) \to (pc3_left c t3 t5))))).(\lambda (t5: T).(\lambda
-(H3: (pc3_left c t4 t5)).(let TMP_3 \def (H2 t5 H3) in (pc3_left_ur c t0 t3
-H0 t5 TMP_3)))))))))) in (let TMP_6 \def (\lambda (t0: T).(\lambda (t3:
-T).(\lambda (H0: (pr2 c t0 t3)).(\lambda (t4: T).(\lambda (_: (pc3_left c t0
-t4)).(\lambda (H2: ((\forall (t5: T).((pc3_left c t4 t5) \to (pc3_left c t0
-t5))))).(\lambda (t5: T).(\lambda (H3: (pc3_left c t4 t5)).(let TMP_5 \def
-(H2 t5 H3) in (pc3_left_ux c t0 t3 H0 t5 TMP_5)))))))))) in (pc3_left_ind c
-TMP_1 TMP_2 TMP_4 TMP_6 t1 t2 H)))))))).
+t2)).(pc3_left_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (t3:
+T).((pc3_left c t0 t3) \to (pc3_left c t t3))))) (\lambda (t: T).(\lambda
+(t3: T).(\lambda (H0: (pc3_left c t t3)).H0))) (\lambda (t0: T).(\lambda (t3:
+T).(\lambda (H0: (pr2 c t0 t3)).(\lambda (t4: T).(\lambda (_: (pc3_left c t3
+t4)).(\lambda (H2: ((\forall (t5: T).((pc3_left c t4 t5) \to (pc3_left c t3
+t5))))).(\lambda (t5: T).(\lambda (H3: (pc3_left c t4 t5)).(pc3_left_ur c t0
+t3 H0 t5 (H2 t5 H3)))))))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0:
+(pr2 c t0 t3)).(\lambda (t4: T).(\lambda (_: (pc3_left c t0 t4)).(\lambda
+(H2: ((\forall (t5: T).((pc3_left c t4 t5) \to (pc3_left c t0
+t5))))).(\lambda (t5: T).(\lambda (H3: (pc3_left c t4 t5)).(pc3_left_ux c t0
+t3 H0 t5 (H2 t5 H3)))))))))) t1 t2 H)))).