Nuprl - Proof: inj imp le2 1 1 1

(4steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. m :

2. k :

3. (

f:(

m

k). Inj(

m;

k; f))

m

k
4. f :

m

k
5. Inj(

m;

k; f)

f:(

m

k). Inj(

m;

k; f)

By:	Witness: f

Generated subgoals:

None

About:

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

(4steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc