Nuprl - Pf mn_23_lem

1. P: Prop
2. n:
3. k:{n...}. P(k) (i:k. P(i))
4. m:
5. P(m)
6. m < n

m:n. P(m)

By: Assert (i:(m-n+2). l:(m-i+1). P(l))

Generated subgoals:

1 i:(m-n+2). l:(m-i+1). P(l)

2 7. i:(m-n+2). l:(m-i+1). P(l)
m:n. P(m)

About:

1	`i:(m-n+2). l:(m-i+1). P(l)`
2	7. `i:(m-n+2). l:(m-i+1). P(l)` `m:n. P(m)`