---

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


1. f : Top
2. b : bag(Top)
3. f@ {} b ~ {}
4. ∀[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 ⌜1⌝ (D 0)⋅ THEN RepUR ``bag-null empty-bag`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  f  :  Top
2.  b  :  bag(Top)
3.  f@  \{\}  b  \msim{}  \{\}
4.  \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{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  RepUR  ``bag-null  empty-bag``  0  THEN  Auto)\mcdot{}

---

Home Index