---

Step * 1 of Lemma lifting-3-strict


1. f : Top
2. b : bag(Top)
3. b' : bag(Top)@i
4. ∀[a:k:ℕ3 ⟶ bag(Top)]. lifting-gen-rev(3;f;a) ~ {} supposing ∃k:ℕ3. (↑bag-null(a k))
⊢ ∃k:ℕ3. (↑bag-null([{}; b; 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.  b'  :  bag(Top)@i
4.  \mforall{}[a:k:\mBbbN{}3  {}\mrightarrow{}  bag(Top)].  lifting-gen-rev(3;f;a)  \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{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  RepUR  ``bag-null  empty-bag``  0  THEN  Auto)\mcdot{}

---

Home Index