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 =
Show proof