---

Step * of Lemma empty-sub-bag

∀T:Type. ∀b:bag(T).  sub-bag(T;{};b)
BY
{ (Auto THEN With ⌜b⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}b:bag(T).    sub-bag(T;\{\};b)


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index