Nuprl - Proof: fin plus nat ooc nat 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fin plus nat ooc nat 1

1. k :

(

) ~

By:	Witness: d.InjCase(d; i. i; n. k+n) \| j.if j<k inl(j) else inr(j-k) fi

Generated subgoals:

1   (j.if j<k inl(j) else inr(j-k) fi)  (k+)
1 step

2   InvFuns(k+;
  InvFuns;d.InjCase(d; i. i; n. k+n);j.if j<k inl(j) else inr(j-k) fi)
5 steps

About:

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

1	(j.if j<k inl(j) else inr(j-k) fi) (k+)	1 step
2	InvFuns(k+; InvFuns;d.InjCase(d; i. i; n. k+n);j.if j<k inl(j) else inr(j-k) fi)	5 steps