INDUCTIVE DEFINITION csubst1 () [ :nat, :T, :C ]
OF ARITY C→Prop
BUILT FROM:
     csubst1_refl: csubst1 i v c1 c1
   | csubst1_sing: ∀c2:C.(csubst0 i v c1 c2)→(csubst1 i v c1 c2)