INDUCTIVE DEFINITION fsubst0 () [ :nat, :T, :C, :T ]
OF ARITY C→T→Prop
BUILT FROM:
     fsubst0_snd: ∀t2:T.(subst0 i v t1 t2)→(fsubst0 i v c1 t1 c1 t2)
   | fsubst0_fst: ∀c2:C.(csubst0 i v c1 c2)→(fsubst0 i v c1 t1 c2 t1)
   | fsubst0_both: ∀t2:T.(subst0 i v t1 t2)→∀c2:C.(csubst0 i v c1 c2)→(fsubst0 i v c1 t1 c2 t2)