DEFINITION sc3_abst()
TYPE =
       ∀g:G
         .∀a:A
           .∀vs:TList
             .∀c:C
               .∀i:nat
                 .arity g c (THeads (Flat Appl) vs (TLRef i)) a
                   →(nf2 c (TLRef i)
                        →(sns3 c vs)→(sc3 g a c (THeads (Flat Appl) vs (TLRef i))))
BODY =
        assume g: G
        assume a: A
        assume vs: TList
        assume c: C
        assume i: nat
        suppose H: arity g c (THeads (Flat Appl) vs (TLRef i)) a
        suppose H0: nf2 c (TLRef i)
        suppose H1: sns3 c vs
          (H_x) 
             by (sc3_props__sc3_sn3_abst . .)

                land
                  ∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
                  ∀vs:TList
                    .∀i:nat
                      .let t := THeads (Flat Appl) vs (TLRef i)
                      in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)
          end of H_x
          (H2) consider H_x
          consider H2
          we proved 
             land
               ∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
               ∀vs:TList
                 .∀i:nat
                   .let t := THeads (Flat Appl) vs (TLRef i)
                   in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)
          that is equivalent to 
             land
               ∀c0:C.∀t:T.(sc3 g a c0 t)→(sn3 c0 t)
               ∀vs0:TList
                 .∀i0:nat
                   .∀c0:C
                     .arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a
                       →(nf2 c0 (TLRef i0)
                            →(sns3 c0 vs0)→(sc3 g a c0 (THeads (Flat Appl) vs0 (TLRef i0))))
          we proceed by induction on the previous result to prove sc3 g a c (THeads (Flat Appl) vs (TLRef i))
             case conj : :∀c0:C.∀t:T.(sc3 g a c0 t)→(sn3 c0 t) H4:∀vs0:TList.∀i0:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a)→(nf2 c0 (TLRef i0))→(sns3 c0 vs0)→(sc3 g a c0 (THeads (Flat Appl) vs0 (TLRef i0))) ⇒
                the thesis becomes sc3 g a c (THeads (Flat Appl) vs (TLRef i))
                   by (H4 . . . H H0 H1)
sc3 g a c (THeads (Flat Appl) vs (TLRef i))
          we proved sc3 g a c (THeads (Flat Appl) vs (TLRef i))
       we proved 
          ∀g:G
            .∀a:A
              .∀vs:TList
                .∀c:C
                  .∀i:nat
                    .arity g c (THeads (Flat Appl) vs (TLRef i)) a
                      →(nf2 c (TLRef i)
                           →(sns3 c vs)→(sc3 g a c (THeads (Flat Appl) vs (TLRef i))))