PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
decide
imp
bool
1
2
1.
T:
Type
2.
R:
T
T
Prop
3.
x,y:T. Dec(x R y)
4.
f:(T
T
).
x,z:T. f(x,z)
(x R z)
r:(T
T
).
x,y:T. (x r y)
(x R y)
By:
Unfold `infix_ap` 0
Generated subgoals:
None
About:
TProp
x,y:T. Dec(x R y)
f:(TT
). x,z:T. f(x,z) 
(x R z)
r:(TT). x,y:T. (x r y) (x R y)