DEFINITION sc3_arity_csubc()
TYPE =
       ∀g:G
         .∀c1:C
           .∀t:T
             .∀a:A
               .arity g c1 t a
                 →∀d1:C.∀is:PList.(drop1 is d1 c1)→∀c2:C.(csubc g d1 c2)→(sc3 g a c2 (lift1 is t))
BODY =
Show proof