{
[T:Type].
(Normal(T)
)
}
{
Proof
}
Definitions occuring in Statement
:
normal-type:
Normal(T)
,
uall:
[x:A].
B[x]
,
prop:
,
member:
t
T
,
universe:
Type
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
prop:
,
normal-type:
Normal(T)
\mforall{}[T:Type]. (Normal(T) \mmember{} \mBbbP{})
Date html generated: 2011_08_10-AM-08_12_48
Last ObjectModification: 2011_06_18-AM-08_27_48
Home
Index
[x:A]. B[x], [T:Type]. (Normal(T) 
) }[x:A]. B[x], , T, [x:A]. B[x], T, ,