Nuprl - Proof: assert-has-src 3

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

1. i : Id
2. k : Knd
3. isrcv(k) & source(lnk(k)) = i

has-src(i;k)

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

Generated subgoals:

None

About:

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