A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0)
k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S
n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0)
k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S
n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus
gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc
gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus
gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc
gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
(next_plus gz n n0) (plus n0 n))) (refl_equal nat n) (\lambda (n0:
nat).(\lambda (H: (eq nat (next_plus gz n n0) (plus n0 n))).(f_equal nat nat
S (next_plus gz n n0) (plus n0 n) H))) h)).
(next_plus gz n n0) (plus n0 n))) (refl_equal nat n) (\lambda (n0:
nat).(\lambda (H: (eq nat (next_plus gz n n0) (plus n0 n))).(f_equal nat nat
S (next_plus gz n n0) (plus n0 n) H))) h)).
A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4:
A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4
a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4:
A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4
a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
A).(\lambda (a3: A).(\lambda (_: (leqz a0 a3)).(\lambda (H1: (leq gz a0
a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leqz a4 a5)).(\lambda
(H3: (leq gz a4 a5)).(leq_head gz a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
A).(\lambda (a3: A).(\lambda (_: (leqz a0 a3)).(\lambda (H1: (leq gz a0
a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leqz a4 a5)).(\lambda
(H3: (leq gz a4 a5)).(leq_head gz a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).