DEFINITION fsubst0_gen_base()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀t1:T
             .∀t2:T
               .∀v:T
                 .∀i:nat
                   .fsubst0 i v c1 t1 c2 t2
                     →(or3
                          land (eq C c1 c2) (subst0 i v t1 t2)
                          land (eq T t1 t2) (csubst0 i v c1 c2)
                          land (subst0 i v t1 t2) (csubst0 i v c1 c2))
BODY =
Show proof