(3steps total) PrintForm bool 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ifthenelse wf 1 1

1. b : Unit+Unit
2. A : Type
3. p : A
4. q : A
  InjCase(b ; pq A


By: Analyze 1 THEN Reduce 0


Generated subgoals:

None

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

(3steps total) PrintForm bool 1 Sections StandardLIB Doc