{ 
[A,B,C:Type]. [f:A 
B bag(C)]. (f@ 
bag(A) bag(B) bag(C)) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-2: f@,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type,
bag: bag(T)
Lemmas :
bag_wf,
concat-lifting2_wf
\mforall{}[A,B,C:Type]. \mforall{}[f:A {}\mrightarrow{} B {}\mrightarrow{} bag(C)]. (f@ \mmember{} bag(A) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(C))
Date html generated:
2011_08_17-PM-06_10_58
Last ObjectModification:
2011_07_04-PM-09_38_34
Home
Index