DEFINITION arity_gen_cast()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t:T
               .∀a:A
                 .arity g c (THead (Flat Cast) u t) a
                   →land (arity g c u (asucc g a)) (arity g c t a)
BODY =
Show proof