{
[i,j,x:Id].
(link_x
from
i
to
j
IdLnk)
}
{
Proof
}
Definitions occuring in Statement
:
vlnk:
link_x
from
i
to
j
,
IdLnk:
IdLnk
,
Id:
Id
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
IdLnk:
IdLnk
,
vlnk:
link_x
from
i
to
j
Lemmas
:
Id_wf
\mforall{}[i,j,x:Id]. (link\_x from i to j \mmember{} IdLnk)
Date html generated: 2011_08_10-AM-07_47_20
Last ObjectModification: 2011_06_18-AM-08_12_45
Home
Index
[x:A]. B[x], [i,j,x:Id]. (link_x from i to j 
IdLnk) }[x:A]. B[x], T[x:A]. B[x], T,