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

1. T: Type
2. P: TProp
3. g: x:TP(x)+(P(x)False)
4. x: T
5. y: P(x)+(P(x)False)
6. y = g(x)

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

By: RevHypSubst 6 0 THEN Analyze 5 THEN Reduce 0

Generated subgoal:

1 5. y1: P(x)False
6. inr(y1) = g(x)
7. P(x)
False

About: