Nuprl - Proof: hcond def 1 1 1 1 2

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

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

t2 = (@x:'a. ((False

x = t1) & (false

= false

x = 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 : 'a
5. False  x = t1
6. false = false  x = t2
  t2 = x
1 step

About:

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