{
[eq1,eq2,f,x:Top].
(f(x)
~
f(x))
}
{
Proof
}
Definitions occuring in Statement
:
fpf-ap:
f(x)
,
uall:
[x:A].
B[x]
,
top:
Top
,
sqequal:
s
~
t
Definitions
:
uall:
[x:A].
B[x]
,
fpf-ap:
f(x)
,
member:
t
T
Lemmas
:
top_wf
\mforall{}[eq1,eq2,f,x:Top]. (f(x) \msim{} f(x))
Date html generated: 2011_08_10-AM-07_55_33
Last ObjectModification: 2011_06_18-AM-08_16_44
Home
Index
[x:A]. B[x], [eq1,eq2,f,x:Top]. (f(x) ~ f(x)) }[x:A]. B[x], [x:A]. B[x], 
T