bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)
\to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_n_S n0 n (H
n0 H1))))) y)))) x).
bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)
\to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_n_S n0 n (H
n0 H1))))) y)))) x).