Nuprl - Proof: bool sq 1 1 2

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

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

x ~ y

By:	Analyze 1 THEN Analyze 2 THEN AbReduce 4 THEN AbReduce 5 THEN Try (Analyze 6 THEN Eq)

Generated subgoals:

None

About:

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