INDUCTIVE DEFINITION csubst0 () [ ]
OF ARITY nat→T→C→C→Prop
BUILT FROM:
     csubst0_snd: ∀k:K.∀i:nat.∀v:T.∀u1:T.∀u2:T.(subst0 i v u1 u2)→∀c:C.(csubst0 (s k i) v (CHead c k u1) (CHead c k u2))
   | csubst0_fst: ∀k:K.∀i:nat.∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀u:T.(csubst0 (s k i) v (CHead c1 k u) (CHead c2 k u))
   | csubst0_both: ∀k:K
                               .∀i:nat
                                 .∀v:T.∀u1:T.∀u2:T.(subst0 i v u1 u2)→∀c1:C.∀c2:C.(csubst0 i v c1 c2)→(csubst0 (s k i) v (CHead c1 k u1) (CHead c2 k u2))