(t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2:
A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4:
(arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u
(t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2:
A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4:
(arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u