{
[T:Id
Type].
(data(T)
Type)
}
{
Proof
}
Definitions occuring in Statement
:
data:
data(T)
,
Id:
Id
,
uall:
[x:A].
B[x]
,
member:
t
T
,
function:
x:A
B[x]
,
universe:
Type
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
data:
data(T)
Lemmas
:
Id_wf
\mforall{}[T:Id {}\mrightarrow{} Type]. (data(T) \mmember{} Type)
Date html generated: 2011_08_16-AM-10_58_45
Last ObjectModification: 2011_06_18-AM-09_32_37
Home
Index
[x:A]. B[x], [T:Id 
Type]. (data(T) 
Type) }[x:A]. B[x], T, B[x], [x:A]. B[x], T,