\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
t1 t2) \to (ex2 A (\lambda (a1: A).(arity g c t1 a1)) (\lambda (a1: A).(arity
g c t2 (asucc g a1))))))))
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
t1 t2) \to (ex2 A (\lambda (a1: A).(arity g c t1 a1)) (\lambda (a1: A).(arity
g c t2 (asucc g a1))))))))