{
[a:Atom1].
[l:IdLnk].
l:IdLnk||a
}
{
Proof
}
Definitions occuring in Statement
:
IdLnk:
IdLnk
,
uall:
[x:A].
B[x]
,
free-from-atom:
x:T||a
,
atom:
Atom$n
Definitions
:
uall:
[x:A].
B[x]
,
IdLnk:
IdLnk
,
member:
t
T
Lemmas
:
free-from-atom-Id
,
Id_wf
\mforall{}[a:Atom1]. \mforall{}[l:IdLnk]. l:IdLnk||a
Date html generated: 2011_08_10-AM-07_43_35
Last ObjectModification: 2011_06_18-AM-08_10_05
Home
Index
[x:A]. B[x], [a:Atom1]. [l:IdLnk]. l:IdLnk||a }[x:A]. B[x], [x:A]. B[x], 
T