DEFINITION sc3()
TYPE =
       G→A→C→T→Prop
BODY =
FIXsc3{
         sc3:G→A→C→T→Prop
         :=λg:G
           .λa:A
             .λc:C
               .λt:T
                 .<λa1:A.Prop>
                   CASE a OF
                     ASort h n⇒land (arity g c t (ASort h n)) (sn3 c t)
                   | AHead a1 a2⇒
                         land
                           arity g c t (AHead a1 a2)
                           ∀d:C
                             .∀w:T
                               .sc3 g a1 d w
                                 →∀is:PList.(drop1 is d c)→(sc3 g a2 d (THead (Flat Appl) w (lift1 is t)))
         }