Nuprl - Proof: bool sq 1 1 1 1

(6steps total) PrintForm sqequal 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bool sq 1 1 1 1

1. x : Unit+Unit
2. y : Unit+Unit
3. x = y
4. InjCase[x]( x ; x) = InjCase(y; x. x, x)
5. InjCase[x]( True ; False) = InjCase(y; x. True, False)
6. True = False

False

By:	RevHypSubst -1 0

Generated subgoals:

None

About:

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

(6steps total) PrintForm sqequal 1 Sections StandardLIB Doc