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

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. T : Type
2. E : T

Prop
3.

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

6. b

E(x)

b':

. (b'

E(x))

b' = b

By:	Rewrite by b E(x)

Generated subgoal:

1 b':. (b' b) b' = b
1 step

About:

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