Nuprl - Proof: hsum iso def 1 2 2 1 1 3 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum iso def 1 2 2 1 1 3 1

1. 'a : S
2. 'b : S
3. x : 'a
4. y : 'b
5.

True

inl(x) = inr(y)

'a+'b

By:	Simpsetp [`nlogic`]

Generated subgoals:

None

About:

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