INDUCTIVE DEFINITION wcpr0 () [ ]
OF ARITY C→C→Prop
BUILT FROM:
     wcpr0_refl: ∀c:C.(wcpr0 c c)
   | wcpr0_comp: ∀c1:C.∀c2:C.(wcpr0 c1 c2)→∀u1:T.∀u2:T.(pr0 u1 u2)→∀k:K.(wcpr0 (CHead c1 k u1) (CHead c2 k u2))