Nuprl - Proof: better-w-match-exists 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: better-w-match-exists 1 1

1. the_w : World
2. e1 : Id
3. e2 :

isnull(a(e1;e2)) [not for witness]
5. isrcv(kind(a(e1;e2)))

isnull(a(e1;e2))

isrcv(kind(a(e1;e2)))

lnk(kind(a(e1;e2))) = lnk(kind(a(e1;e2)))

By:	Unhide THEN AutoBoolCase isnull(a(e1;e2)) THEN AutoBoolCase isrcv(kind(a(e1;e2)))

Generated subgoal:

1 4. isnull(a(e1;e2))
5. isrcv(kind(a(e1;e2)))
6. isnull(a(e1;e2))
7. isrcv(kind(a(e1;e2)))
lnk(kind(a(e1;e2))) = lnk(kind(a(e1;e2)))
1 step

About:

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