PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
decide
imp
bool
1
1
1
1.
T:
Type
2.
R:
T
T
Prop
3.
x,y:T. Dec(x R y)
4.
x:
T
y:(T
).
z:T. y(z)
(x R z)
By:
Inst
Thm*
Q:(A
B
Prop). (
x:A.
y:B. Q(x,y))
(
f:(A
B).
x:A. Q(x,f(x))) [T;
;
z,y. y
(x R z)]
Generated subgoal:
1
x@0:T.
y:
. y
(x R x@0)
About:
x@0:T. 
y:
. y 
(x R x@0)
TPropx,y:T. Dec(x R y) y:(T). z:T. y(z) (x R z)Q:(ABProp). (x:A. y:B. Q(x,y)) 
(f:(AB). x:A. Q(x,f(x)))
[T;;
z,y. y (x R z)] x@0:T. y:. y (x R x@0)
