---

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


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index