{
[a,b:Knd].
(a
=
b
)
}
{
Proof
}
Definitions occuring in Statement
:
eq_knd:
a
=
b
,
Knd:
Knd
,
bool:
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
eq_knd:
a
=
b
Lemmas
:
eqof_wf
,
Knd_wf
,
Kind-deq_wf
\mforall{}[a,b:Knd]. (a = b \mmember{} \mBbbB{})
Date html generated: 2011_08_10-AM-07_49_19
Last ObjectModification: 2011_06_18-AM-08_13_29
Home
Index
, 
[a,b:Knd]. (a = b 
) }, [x:A]. B[x], T[x:A]. B[x], T,