Nuprl - Proof: dec pred iff some boolfun 1 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

1. T : Type
2. E : T

Prop
3.

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

6. b

E(x)

b is the b:

. b

E(x)

By:	Analyze THEN CBV: b'

Generated subgoals:

1 b E(x)
Hypothesis

2 b':. (b' E(x)) b' = b
2 steps

About:

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