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