---

Step * of Lemma remove-repeats-l_contains-iff

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List.  (as ⊆ bs ⇐⇒ remove-repeats(eq;as) ⊆ remove-repeats(eq;bs))
BY
{ ((RepeatFor 4 ((D 0 THENA Auto)) THEN (RWO "l_subset-l_contains<" 0 THENA Auto))
   THEN Unfold `l_subset` 0
   THEN RWO  "member-remove-repeats" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.    (as  \msubseteq{}  bs  \mLeftarrow{}{}\mRightarrow{}  remove-repeats(eq;as)  \msubseteq{}  remove-repeats(eq;bs))


By

---

Latex:
((RepeatFor  4  ((D  0  THENA  Auto))  THEN  (RWO  "l\_subset-l\_contains<"  0  THENA  Auto))
  THEN  Unfold  `l\_subset`  0
  THEN  RWO    "member-remove-repeats"  0
  THEN  Auto)

---

Home Index