(2steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: locl one one 1
1. a : Id
2. b : Id
3. inr(a) = inr(b)
  a = b
By: Obvious

Generated subgoals:

None

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

(2steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc