---

Step * of Lemma bag-no-repeats-list

∀[T:Type]. ∀[L:T List].  uiff(bag-no-repeats(T;L);no_repeats(T;L))
BY
{ (Auto THEN All(Unfold `bag-no-repeats`)) }

1
1. T : Type
2. L : T List
3. ↓∃L@0:T List. ((L@0 = L ∈ bag(T)) ∧ no_repeats(T;L@0))
⊢ no_repeats(T;L)

2
1. T : Type
2. L : T List
3. no_repeats(T;L)
⊢ ↓∃L@0:T List. ((L@0 = L ∈ bag(T)) ∧ no_repeats(T;L@0))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    uiff(bag-no-repeats(T;L);no\_repeats(T;L))


By

---

Latex:
(Auto  THEN  All(Unfold  `bag-no-repeats`))

---

Home Index