nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).(\forall (k:
nat).((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (P
(ASort h1 n1) (ASort h2 n2))))))))) (f0: (\forall (a1: A).(\forall (a2:
nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).(\forall (k:
nat).((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (P
(ASort h1 n1) (ASort h2 n2))))))))) (f0: (\forall (a1: A).(\forall (a2: