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