Nuprl - Proof: dec pred imp bool decider exists 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dec pred imp bool decider exists 1

1. A : Type
2. P : A

Type
3.

x:A. Dec(P(x))
4.

f:(A

x:A. f(x)

P(x)

{p:(A

x:A. p(x)

P(x) }

By:	Analyze-1 THEN Witness: f THEN Rename-1: g THEN Analyze-1

Generated subgoal:

1 4. f : A
5. x:A. f(x)  P(x)
6. g : A
7. x:A. g(x)  P(x)
  f = g  {p:(A)| x:A. p(x)  P(x) }
4 steps

About:

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