DEFINITION fsubst0_ind()
TYPE =
       ∀i:nat
         .∀v:T
           .∀c1:C
             .∀t1:T
               .∀P:C→T→Prop
                 .∀t:T.(subst0 i v t1 t)→(P c1 t)
                   →(∀c:C.(csubst0 i v c1 c)→(P c t1)
                        →(∀t:T.(subst0 i v t1 t)→∀c:C.(csubst0 i v c1 c)→(P c t)
                             →∀c:C.∀t:T.(fsubst0 i v c1 t1 c t)→(P c t)))
BODY =
Show proof