Nuprl - Pf decidable iff exists bool function 2 1 1 1 1

1. T: Type
2. Z: Type
3. P: TZProp
4. g: x:Ty:ZP(x,y)+(P(x,y) False)
5. x: T
6. y: Z

P(x,y) InjCase(g(x,y) ; true; false)

By: Witness4 x

Generated subgoal:

1 7. y1: y:ZP(x,y)+(P(x,y) False)
8. y1 = g(x)
P(x,y) InjCase(g(x,y) ; true; false)

About: