---

Step * 1 of Lemma concat-lifting-2-strict


1. f : Top
2. b : bag(Top)
3. ∀[a:k:ℕ2 ⟶ bag(Top)]. lifting-gen-list-rev(2;a) 0 f ~ {} supposing ∃k:ℕ2. (↑bag-null(a k))
⊢ ∃k:ℕ2. (↑bag-null([{}; b][k]))
BY
{ (With ⌜0⌝ (D 0)⋅ THEN RepUR ``bag-null empty-bag`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  f  :  Top
2.  b  :  bag(Top)
3.  \mforall{}[a:k:\mBbbN{}2  {}\mrightarrow{}  bag(Top)].  lifting-gen-list-rev(2;a)  0  f  \msim{}  \{\}  supposing  \mexists{}k:\mBbbN{}2.  (\muparrow{}bag-null(a  k))
\mvdash{}  \mexists{}k:\mBbbN{}2.  (\muparrow{}bag-null([\{\};  b][k]))


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  RepUR  ``bag-null  empty-bag``  0  THEN  Auto)\mcdot{}

---

Home Index