\forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq
g (ASort h1 n1) a2) \to (ex2_3 nat nat nat (\lambda (n2: nat).(\lambda (h2:
nat).(\lambda (k: nat).(eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2)
\forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq
g (ASort h1 n1) a2) \to (ex2_3 nat nat nat (\lambda (n2: nat).(\lambda (h2:
nat).(\lambda (k: nat).(eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2)