DEFINITION sc3_props__sc3_sn3_abst()
TYPE =
       ∀g:G
         .∀a:A
           .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)
BODY =
Show proof