---

Step * of Lemma bag-no-repeats-subtype

∀[T,A:Type]. ∀[bs:bag(A)].  (bag-no-repeats(A;bs)) supposing (bag-no-repeats(T;bs) and strong-subtype(A;T))
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN ExRepD) }

1
1. T : Type
2. A : Type
3. bs : bag(A)
4. strong-subtype(A;T)
5. L : T List
6. L = bs ∈ bag(T)
7. no_repeats(T;L)
⊢ ∃L:A List. ((L = bs ∈ bag(A)) ∧ no_repeats(A;L))

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[bs:bag(A)].
    (bag-no-repeats(A;bs))  supposing  (bag-no-repeats(T;bs)  and  strong-subtype(A;T))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  ExRepD)

---

Home Index