---

Step * 1 of Lemma member-insert-no-combine


1. T : Type
2. cmp : comparison(T)
3. x : T
4. z : T
⊢ (z ∈ [x]) ⇐⇒ (z ∈ [x])
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  x  :  T
4.  z  :  T
\mvdash{}  (z  \mmember{}  [x])  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  [x])


By

---

Latex:
Auto

---

Home Index