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 =
        assume i: nat
        assume v: T
        assume c1: C
        assume t1: T
        assume P: C→T→Prop
        suppose H: ∀t:T.(subst0 i v t1 t)→(P c1 t)
        suppose H1: ∀c:C.(csubst0 i v c1 c)→(P c t1)
        suppose H2: ∀t:T.(subst0 i v t1 t)→∀c:C.(csubst0 i v c1 c)→(P c t)
        assume c: C
        assume t: T
        suppose H3: fsubst0 i v c1 t1 c t
          by cases on H3 we prove P c t
             case fsubst0_snd t2:T H4:subst0 i v t1 t2 ⇒
                the thesis becomes P c1 t2
                by (H . H4)
P c1 t2
             case fsubst0_fst c2:C H4:csubst0 i v c1 c2 ⇒
                the thesis becomes P c2 t1
                by (H1 . H4)
P c2 t1
             case fsubst0_both t2:T H4:subst0 i v t1 t2 c2:C H5:csubst0 i v c1 c2 ⇒
                the thesis becomes P c2 t2
                by (H2 . H4 . H5)
P c2 t2
          we proved P c t
       we proved 
          ∀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)))