Nuprl - Proof: dec pred iff some boolfun 1 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dec pred iff some boolfun 1 1 1 1 2 1

1. T : Type
2. E : T

Prop
3.

x:T. Dec(E(x))
4. x : T
5. b :

6. b

E(x)

b':

. (b'

b' = b

By:	2 Times Analyze THEN BackThru: Thm* a,b:. (a b) a = b

Generated subgoals:

None

About:

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