---

Step * of Lemma concat-lifting-loc-member

∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[bags:k:ℕn ─→ bag(A k)]. ∀[f:Id ─→ funtype(n;A;bag(B))]. ∀[b:B]. ∀[l:Id].
  (b ↓∈ concat-lifting-loc(n;bags;l;f)
  ⇐⇒ ↓∃lst:k:ℕn ─→ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f l) lst))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `concat-lifting-loc` 0
   THEN InstLemma `concat-lifting-member` [⌈B⌉; ⌈n⌉; ⌈A⌉; ⌈bags⌉; ⌈f l⌉; ⌈b⌉]⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].  \mforall{}[f:Id  {}\mrightarrow{}  funtype(n;A;bag(B))].
\mforall{}[b:B].  \mforall{}[l:Id].
    (b  \mdownarrow{}\mmember{}  concat-lifting-loc(n;bags;l;f)
    \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}lst:k:\mBbbN{}n  {}\mrightarrow{}  (A  k).  ((\mforall{}[k:\mBbbN{}n].  lst  k  \mdownarrow{}\mmember{}  bags  k)  \mwedge{}  b  \mdownarrow{}\mmember{}  uncurry-rev(n;f  l)  lst))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `concat-lifting-loc`  0
  THEN  InstLemma  `concat-lifting-member`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}bags\mkleeneclose{};  \mkleeneopen{}f  l\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index