DEFINITION sc3_arity()
TYPE =
       g:G.c:C.t:T.a:A.(arity g c t a)(sc3 g a c t)
BODY =
Show proof