(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum iso def 1 2 2 1 1 4 1

1. 'a : S
2. 'b : S
3. y1 : 'b
4. y : 'b
5. y1 = y
  inr(y1) = inr(y 'a+'b


By: Analyze


Generated subgoals:

None

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

(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc