DEFINITION sc3_arity()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀a:A.(arity g c t a)→(sc3 g a c t)
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume a: A
        suppose H: arity g c t a
          (H_y) 
             by (sc3_arity_csubc . . . . H . .)
(drop1 PNil c c)→∀c2:C.(csubc g c c2)→(sc3 g a c2 (lift1 PNil t))
          end of H_y
          (h1) 
             by (drop1_nil .)
drop1 PNil c c
          end of h1
          (h2) 
             by (csubc_refl . .)
csubc g c c
          end of h2
          by (H_y h1 . h2)
          we proved sc3 g a c (lift1 PNil t)
          that is equivalent to sc3 g a c t
       we proved ∀g:G.∀c:C.∀t:T.∀a:A.(arity g c t a)→(sc3 g a c t)