DEFINITION ty3_arity()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ex2 A λa1:A.arity g c t1 a1 λa1:A.arity g c t2 (asucc g a1))
BODY =
Show proof