(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
iff
exists
bool
function
2
1
1
1.
T:
Type
2.
Z:
Type
3.
P:
T
Z
Prop
4.
g:
x:T
y:Z
P(x,y)+(P(x,y)
False)
f_p:(T
Z
).
x:T, y:Z. P(x,y)
f_p(x,y)
By:
Witness
x,y. InjCase(g(x,y) ; true
; false
)
THEN
Analyze 0
THEN
Reduce 0
Generated subgoal:
1
5.
x:
T
y:Z. P(x,y)
InjCase(g(x,y) ; true
; false
)
About:
(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
y:Z. P(x,y) 
InjCase(g(x,y) ; true
; false)
ZProp
y:ZP(x,y)+(P(x,y) 
False)
f_p:(TZ
). x:T, y:Z. P(x,y) f_p(x,y)
x,y. InjCase(g(x,y) ; true; false)
y:Z. P(x,y) InjCase(g(x,y) ; true; false)
