(\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P (CHead
c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on w: P c
c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp c1 c2
w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1 u2 p
k)].
(\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P (CHead
c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on w: P c
c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp c1 c2
w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1 u2 p
k)].