Nuprl - Proof: inj imp le 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inj imp le 1

1. m :

2. 0<m
3.

k':

. (

f':(

(m-1)

k'). Inj(

(m-1);

k'; f'))

m-1

k'
4. k :

f:(

k). Inj(

k; f)

By:

Analyze5

Generated subgoal:

1 5. f : mk
6. Inj(m; k; f)
mk
5 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html