Nuprl - Proof: assert-has-src 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-has-src 1

1. i : Id
2. k : Knd
3. has-src(i;k)

isrcv(k)

By:	DVar `k' THEN Repeat (Unfolds [`has-src`;`isrcv`] -1 THEN Reduce -1) THEN Unfold `isrcv` 0 THEN Reduce 0

Generated subgoals:

None

About:

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