Nuprl - Proof: assert-has-src 2

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

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

source(lnk(k)) = i

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

Generated subgoals:

None

About:

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