(a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (csuba g
c2 c)).(\lambda (H4: (csubv c2 c)).(arity_repl g c2 t0 a1 (H1 c2 H3 H4) a2
H2))))))))))) c1 t a H))))).
(a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (csuba g
c2 c)).(\lambda (H4: (csubv c2 c)).(arity_repl g c2 t0 a1 (H1 c2 H3 H4) a2
H2))))))))))) c1 t a H))))).