---

Step * of Lemma bag-single-no-repeats

∀[T:Type]. ∀[x:T].  bag-no-repeats(T;{x})
BY
{ (Auto THEN Unfold `single-bag` 0 THEN D 0 THEN Auto THEN With ⌜[x]⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].    bag-no-repeats(T;\{x\})


By

---

Latex:
(Auto  THEN  Unfold  `single-bag`  0  THEN  D  0  THEN  Auto  THEN  With  \mkleeneopen{}[x]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index