DEFINITION sc3_sn3()
TYPE =
       ∀g:G.∀a:A.∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
BODY =
        assume g: G
        assume a: A
        assume c: C
        assume t: T
        suppose H: sc3 g a c t
          (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
          (H0) consider H_x
          consider H0
          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.∀t0:T.(sc3 g a c0 t0)→(sn3 c0 t0)
               ∀vs:TList
                 .∀i:nat
                   .∀c0:C
                     .arity g c0 (THeads (Flat Appl) vs (TLRef i)) a
                       →(nf2 c0 (TLRef i)
                            →(sns3 c0 vs)→(sc3 g a c0 (THeads (Flat Appl) vs (TLRef i))))
          we proceed by induction on the previous result to prove sn3 c t
             case conj : H1:∀c0:C.∀t0:T.(sc3 g a c0 t0)→(sn3 c0 t0) :∀vs:TList.∀i:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs (TLRef i)) a)→(nf2 c0 (TLRef i))→(sns3 c0 vs)→(sc3 g a c0 (THeads (Flat Appl) vs (TLRef i))) ⇒
                the thesis becomes sn3 c t
                   by (H1 . . H)
sn3 c t
          we proved sn3 c t
       we proved ∀g:G.∀a:A.∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)