Nuprl - Proof: assert-w-isrcvl

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-w-isrcvl

the_w:World, l:IdLnk, i:Id, a:Action(i).

isrcv(l;a)

isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l

By:	Auto THEN MoveToConcl -1 THEN Unfold `w-isrcvl` 0 THEN AutoBoolCase isnull(a) THEN AutoBoolCase isrcv(kind(a)) THEN Unfold `guard` 0 THEN RWO Thm* a,b:IdLnk. a = b a = b -1

Generated subgoals:

None

About:

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