{
[a,b:IdLnk].
(a
=
b
)
}
{
Proof
}
Definitions occuring in Statement
:
eq_lnk:
a
=
b
,
IdLnk:
IdLnk
,
bool:
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
eq_lnk:
a
=
b
Lemmas
:
eqof_wf
,
IdLnk_wf
,
idlnk-deq_wf
\mforall{}[a,b:IdLnk]. (a = b \mmember{} \mBbbB{})
Date html generated: 2011_08_10-AM-07_48_02
Last ObjectModification: 2011_06_18-AM-08_12_57
Home
Index
, 
[a,b:IdLnk]. (a = b 
) }, [x:A]. B[x], T[x:A]. B[x], T,