T).(\lambda (a: A).(\lambda (H2: (sc3 g (asucc g a) c3 v)).(\lambda (w:
T).(\lambda (H3: (sc3 g a c4 w)).(csuba_abst g c3 c4 H1 v a (sc3_arity_gen g
c3 v (asucc g a) H2) w (sc3_arity_gen g c4 w a H3))))))))))) c1 c2 H)))).
T).(\lambda (a: A).(\lambda (H2: (sc3 g (asucc g a) c3 v)).(\lambda (w:
T).(\lambda (H3: (sc3 g a c4 w)).(csuba_abst g c3 c4 H1 v a (sc3_arity_gen g
c3 v (asucc g a) H2) w (sc3_arity_gen g c4 w a H3))))))))))) c1 c2 H)))).