---

{ [B:Type]. [n:]. [A:n  Type]. [bags:k:n  bag(A k)]. [loc:Id].
  [f:Id  funtype(n;A;B)].
    (lifting-loc-gen-rev(n;bags;loc;f)  bag(B)) }

{ Proof }

---

Definitions occuring in Statement :  lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),  Id: Id,  int_seg: {i..j},  nat: ,  uall: [x:A]. B[x],  member: t  T,  apply: f a,  function: x:A  B[x],  natural_number: $n,  universe: Type,  bag: bag(T),  funtype: funtype(n;A;T)
Definitions :  tactic: Error :tactic,  uall: [x:A]. B[x],  member: t  T,  isect: x:A. B[x],  Id: Id,  function: x:A  B[x],  int_seg: {i..j},  apply: f a,  bag: bag(T),  universe: Type,  nat: ,  equal: s = t,  funtype: funtype(n;A;T),  lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),  axiom: Ax,  all: x:A. B[x],  natural_number: $n,  int: ,  subtype: S  T,  grp_car: |g|,  real: ,  set: {x:A| B[x]} ,  lifting-gen-rev: lifting-gen-rev(n;f;bags)
Lemmas :  lifting-gen-rev_wf,  nat_wf,  int_seg_wf,  bag_wf,  Id_wf,  funtype_wf

---

\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].  \mforall{}[loc:Id].  \mforall{}[f:Id  {}\mrightarrow{}  funtype(n;A;B)].
    (lifting-loc-gen-rev(n;bags;loc;f)  \mmember{}  bag(B))


Date html generated: 2011_08_17-PM-06_04_52
Last ObjectModification: 2011_06_01-PM-07_34_54

Home Index