---

Step * 1 1 1 1 of Lemma bag-induction


1. L : Top List
⊢ L ~ concat(map(λx.[x];L))
BY
{ (Unfold `concat` 0 THEN ListInd 1 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  Top  List
\mvdash{}  L  \msim{}  concat(map(\mlambda{}x.[x];L))


By

---

Latex:
(Unfold  `concat`  0  THEN  ListInd  1  THEN  Reduce  0  THEN  Auto)

---

Home Index