(2steps total) PrintForm core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: top wf 1
  Void(given Void)  Type
By: Unfold `member` 0
THEN
Refine
RULE H   b1(given a1) = b2(given a2)  Type{i}

RULE H BY isectEquality y

RULE H H   a1 = a2  Type{i}
RULE H H, y:a1   b1[y/x1] = b2[y/x2]  Type{i}
RULE H .
[mk_var_arg `x']
THEN
Fold `member` 0

Generated subgoals:

None

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

(2steps total) PrintForm core StandardLIB Doc