t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x
c t1 t0 H) t2 H0)))))).
+theorem pc3_pr3_conf:
+ \forall (c: C).(\forall (t: T).(\forall (t1: T).((pc3 c t t1) \to (\forall
+(t2: T).((pr3 c t t2) \to (pc3 c t2 t1))))))
+\def
+ \lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t
+t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c
+t2 t H0) t1 H)))))).
+
theorem pc3_head_12:
\forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall
(k: K).(\forall (t1: T).(\forall (t2: T).((pc3 (CHead c k u2) t1 t2) \to (pc3