{
[f,i:Top].
(concat-lifting-loc-1(f)
i
{}
~
{})
}
{
Proof
}
Definitions occuring in Statement
:
concat-lifting-loc-1:
concat-lifting-loc-1(f)
,
uall:
[x:A].
B[x]
,
top:
Top
,
apply:
f
a
,
sqequal:
s
~
t
,
empty-bag:
{}
Lemmas
:
subtype_base_sq
,
top_wf
\mforall{}[f,i:Top]. (concat-lifting-loc-1(f) i \{\} \msim{} \{\})
Date html generated: 2011_08_17-PM-06_14_03
Last ObjectModification: 2011_06_28-PM-03_48_15
Home
Index
[x:A]. B[x], [f,i:Top]. (concat-lifting-loc-1(f) i {} ~ {}) }[x:A]. B[x],