PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
1
1
1
2
1
1
1
1
1.
T:
Type
2.
P:
T
Prop
3.
Q:
T
Prop
4.
x:
T
5.
Q(x)
6.
P(x)
Q(x)
x
{t:T| P(t) }
By:
Analyze 6
Generated subgoal:
1
6.
P(x)
Q(x)
7.
(P(x))
(Q(x))
x
{t:T| P(t) }
About:
Q(x)
(Q(x))
x 
{t:T| P(t) }
PropProp Q(x) x {t:T| P(t) } Q(x) (Q(x)) x {t:T| P(t) }
