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 =
        assume c1: C
        assume c2: C
        assume t1: T
        assume t2: T
        assume v: T
        assume i: nat
        suppose H: fsubst0 i v c1 t1 c2 t2
          we proceed by induction on H to prove 
             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)
             case fsubst0_snd : t0:T H0:subst0 i v t1 t0 ⇒
                the thesis becomes 
                or3
                  land (eq C c1 c1) (subst0 i v t1 t0)
                  land (eq T t1 t0) (csubst0 i v c1 c1)
                  land (subst0 i v t1 t0) (csubst0 i v c1 c1)
                   by (refl_equal . .)
                   we proved eq C c1 c1
                   by (conj . . previous H0)
                   we proved land (eq C c1 c1) (subst0 i v t1 t0)
                   by (or3_intro0 . . . previous)

                      or3
                        land (eq C c1 c1) (subst0 i v t1 t0)
                        land (eq T t1 t0) (csubst0 i v c1 c1)
                        land (subst0 i v t1 t0) (csubst0 i v c1 c1)
             case fsubst0_fst : c0:C H0:csubst0 i v c1 c0 ⇒
                the thesis becomes 
                or3
                  land (eq C c1 c0) (subst0 i v t1 t1)
                  land (eq T t1 t1) (csubst0 i v c1 c0)
                  land (subst0 i v t1 t1) (csubst0 i v c1 c0)
                   by (refl_equal . .)
                   we proved eq T t1 t1
                   by (conj . . previous H0)
                   we proved land (eq T t1 t1) (csubst0 i v c1 c0)
                   by (or3_intro1 . . . previous)

                      or3
                        land (eq C c1 c0) (subst0 i v t1 t1)
                        land (eq T t1 t1) (csubst0 i v c1 c0)
                        land (subst0 i v t1 t1) (csubst0 i v c1 c0)
             case fsubst0_both : t0:T H0:subst0 i v t1 t0 c0:C H1:csubst0 i v c1 c0 ⇒
                the thesis becomes 
                or3
                  land (eq C c1 c0) (subst0 i v t1 t0)
                  land (eq T t1 t0) (csubst0 i v c1 c0)
                  land (subst0 i v t1 t0) (csubst0 i v c1 c0)
                   by (conj . . H0 H1)
                   we proved land (subst0 i v t1 t0) (csubst0 i v c1 c0)
                   by (or3_intro2 . . . previous)

                      or3
                        land (eq C c1 c0) (subst0 i v t1 t0)
                        land (eq T t1 t0) (csubst0 i v c1 c0)
                        land (subst0 i v t1 t0) (csubst0 i v c1 c0)
          we proved 
             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)
       we proved 
          ∀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))