PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
decide
imp
bool
1
1
1
1
1
2
1.
T:
Type
2.
R:
T
T
Prop
3.
x,y:T. Dec(x R y)
4.
x:
T
5.
x@0:
T
6.
(x R x@0)
y:
. y
(x R x@0)
By:
Witness false
THEN
Reduce 0
Generated subgoals:
None
About:
TProp
x,y:T. Dec(x R y)
(x R x@0)
y:
. y 
(x R x@0)
