---

Step * of Lemma lifting-loc-member-simple

∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[bags:k:ℕn ─→ bag(A k)]. ∀[f:Id ─→ funtype(n;A;B)]. ∀[b:B]. ∀[l:Id].
  (b ↓∈ lifting-loc-gen-rev(n;bags;l;f)
  ⇐⇒ ↓∃lst:k:ℕn ─→ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ ((uncurry-rev(n;f l) lst) = b ∈ B)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `lifting-loc-gen-rev` 0
   THEN InstLemma `lifting-member-simple` [⌈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;B)].  \mforall{}[b:B].
\mforall{}[l:Id].
    (b  \mdownarrow{}\mmember{}  lifting-loc-gen-rev(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{}  ((uncurry-rev(n;f  l)  lst)  =  b)))


By

---

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

---

Home Index