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