---

Step * 1 of Lemma member-union-list2


1. [T] : Type
2. eq : EqDecider(T)
⊢ ∀x:T. ((x ∈ []) ⇐⇒ ∃l:T List. ((l ∈ []) ∧ (x ∈ l)))
BY
{ (Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mforall{}x:T.  ((x  \mmember{}  [])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}l:T  List.  ((l  \mmember{}  [])  \mwedge{}  (x  \mmember{}  l)))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  Auto)

---

Home Index