PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
0
T:Type, P:(T
Prop). (
x:T. Dec(P(x))) & Dec(
x:T.
P(x))
Dec(
x:T. P(x))
By:
GenUnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
(
x:T. Dec(P(x))) & Dec(
x:T.
P(x))
Dec(
x:T. P(x))
About:
Prop
x:T. Dec(P(x))) & Dec(
x:T. 
P(x))
Dec(x:T. P(x)) T:Type, P:(TProp). (x:T. Dec(P(x))) & Dec(x:T. P(x)) 
Dec(x:T. P(x))Propx:T. Dec(P(x))) & Dec(x:T. P(x)) Dec(x:T. P(x))
