\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2