---

{ [C,B,A:Type]. [f:Id  A  B  bag(C)].
    (f@Loc  Id  bag(A)  bag(B)  bag(C)) }

{ Proof }

---

Definitions occuring in Statement :  concat-lifting-loc-2: f@Loc,  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  universe: Type,  bag: bag(T)
Definitions :  Id: Id,  function: x:A  B[x],  equal: s = t,  axiom: Ax,  concat-lifting-loc-2: f@Loc,  bag: bag(T),  member: t  T,  isect: x:A. B[x],  uall: [x:A]. B[x],  universe: Type,  all: x:A. B[x],  lambda: x.A[x],  concat-lifting2-loc: concat-lifting2-loc(f;abag;bbag;loc)
Lemmas :  bag_wf,  concat-lifting2-loc_wf,  Id_wf

---

\mforall{}[C,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].    (f@Loc  \mmember{}  Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C))


Date html generated: 2011_08_17-PM-06_15_30
Last ObjectModification: 2011_06_02-PM-04_44_37

Home Index