(x: A).(\lambda (H5: (arity g c3 u x)).(\lambda (H6: (arity g c3 t (asucc g
x))).(csuba_abst g c3 c4 H1 t x H6 u (csuba_arity g c3 u x H5 c4 H1)))))
H4))))))))))) c1 c2 H)))).
(x: A).(\lambda (H5: (arity g c3 u x)).(\lambda (H6: (arity g c3 t (asucc g
x))).(csuba_abst g c3 c4 H1 t x H6 u (csuba_arity g c3 u x H5 c4 H1)))))
H4))))))))))) c1 c2 H)))).