Nuprl - Proof: hcond def 1 1 1 1 1

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

1. 'a : S
2. t1 : 'a
3. t2 : 'a

t1 = (@x@0:'a. ((true

= true

x@0 = t1) & (False

x@0 = t2)))

By:	SwapEquands 0 THEN L Thm* P:('aType), x:'a. P(x) (y:'a. P(y) x = y) (@y:'a. P(y)) = x THEN Simp THEN StrongAuto

Generated subgoal:

1 4. x@0 : 'a
5. true = true  x@0 = t1
6. False  x@0 = t2
  t1 = x@0
1 step

About:

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