DEFINITION pc3_ind_left__pc3_pc3_left()
TYPE =
∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→(pc3 c t1 t2)
BODY =
assume c: C
assume t1: T
assume t2: T
suppose H: pc3_left c t1 t2
we proceed by induction on H to prove pc3 c t1 t2
case pc3_left_r : t:T ⇒
the thesis becomes pc3 c t t
by (pc3_refl . .)
pc3 c t t
case pc3_left_ur : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t3 t4 ⇒
the thesis becomes pc3 c t0 t4
(H2) by induction hypothesis we know pc3 c t3 t4
by (pc3_pr2_r . . . H0)
we proved pc3 c t0 t3
by (pc3_t . . . previous . H2)
pc3 c t0 t4
case pc3_left_ux : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t0 t4 ⇒
the thesis becomes pc3 c t3 t4
(H2) by induction hypothesis we know pc3 c t0 t4
by (pc3_pr2_x . . . H0)
we proved pc3 c t3 t0
by (pc3_t . . . previous . H2)
pc3 c t3 t4
we proved pc3 c t1 t2
we proved ∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→(pc3 c t1 t2)