At:
decidable iff exists bool function 2
1
1
1
1
1
1
1
1
1.
T: Type
2.
Z: Type
3.
P: T
ZProp
4.
g: x:Ty:ZP(x,y)+(P(x,y) 
False)
5.
x: T
6.
y: Z
7.
y1: y:ZP(x,y)+(P(x,y) False)
8.
y1 = g(x)
9.
y3: P(x,y) False
10.
inr(y3) = g(x,y)
11.
P(x,y)
False
By:
Analyze 9
Generated subgoals:
None
About:
