(4steps total) PrintForm Definitions union Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: outl wf 1 1
1. A : Type
2. Type
3. x1 : A
4. True
  outl(inl(x1))  A
By: Reduce 0

Generated subgoals:

None

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

(4steps total) PrintForm Definitions union Sections StandardLIB Doc