PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
0
1
1
1.
T:
Type
2.
P:
T
Prop
3.
x:T. Dec(P(x))
4.
Dec(
x:T.
P(x))
Dec(
x:T. P(x))
By:
Unfold `decidable` 0
THEN
Unfold `decidable` 4
Generated subgoal:
1
4.
(
x:T.
P(x))
(
x:T.
P(x))
(
x:T. P(x))
(
x:T. P(x))
About:
x:T. 
P(x)) 
(x:T. P(x))
(
x:T. P(x)) (x:T. P(x))
Propx:T. Dec(P(x))x:T. P(x)) Dec(x:T. P(x))x:T. P(x)) (x:T. P(x)) (x:T. P(x)) (x:T. P(x))
