(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
iff
exists
bool
function
2
1
1.
T:
Type
2.
Z:
Type
3.
P:
T
Z
Prop
4.
x:T, y:Z. Dec(P(x,y))
f_p:(T
Z
).
x:T, y:Z. P(x,y)
f_p(x,y)
By:
Repeat (Unfolds [`decidable`;`or`;`not`;`all`] 4)
THEN
RenameVar `g' 4
Generated subgoal:
1
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)
About:
(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
y:ZP(x,y)+(P(x,y) 
False)
f_p:(TZ
). 
x:T, y:Z. P(x,y) 
f_p(x,y)ZProp
x:T, y:Z. Dec(P(x,y))
f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y)
y:ZP(x,y)+(P(x,y) False) f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y)
