---

Step * of Lemma remove-repeats-wf-bag

∀[T:Type]. ∀eq:EqDecider(T). ∀bs:bag(T).  (remove-repeats(eq;bs) ∈ bag(T))
BY
{ ((UnivCD THENA Auto) THEN D -1 THEN Try (Complete (Auto)) THEN EqTypeCD THEN Auto THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}bs:bag(T).    (remove-repeats(eq;bs)  \mmember{}  bag(T))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1  THEN  Try  (Complete  (Auto))  THEN  EqTypeCD  THEN  Auto  THEN  EAuto  1)

---

Home Index