{ 
[B,A:Type]. [f:A 
bag(B)]. (f@ 
bag(A) bag(B)) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-1: f@,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
universe: Type,
isect: 
x:A. B[x],
member: t T,
axiom: Ax,
equal: s = t,
function: x:A B[x],
concat-lifting-1: f@,
bag: bag(T),
all: x:A. B[x],
lambda: 
x.A[x],
concat-lifting1: concat-lifting1(f;bag)
Lemmas :
bag_wf,
concat-lifting1_wf
\mforall{}[B,A:Type]. \mforall{}[f:A {}\mrightarrow{} bag(B)]. (f@ \mmember{} bag(A) {}\mrightarrow{} bag(B))
Date html generated:
2011_08_17-PM-06_10_36
Last ObjectModification:
2011_06_02-PM-04_41_44
Home
Index