Nuprl - Proof: dec pred iff some boolfun 1 1 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. T : Type
2. E : T

Prop
3.

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

. b

E(x)

!b:

. b

E(x)

By:	SimilarTo Hyp:-1

Generated subgoal:

1 5. b :
6. b E(x)
b is the b:. b E(x)
4 steps

About:

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