---

Step * of Lemma member-list-to-set

∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀a:T.  ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))
BY
{ (InstLemma `list-to-set-property` [] THEN RepeatFor 3 (ParallelLast') THEN D -1 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}a:T.    ((a  \mmember{}  list-to-set(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))


By

---

Latex:
(InstLemma  `list-to-set-property`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  D  -1  THEN  Trivial)

---

Home Index