---

Step * of Lemma l_member-bag-member

∀[T:Type]. ∀x:T. ∀L:T List.  (x ↓∈ L ⇐⇒ ↓(x ∈ L))
BY
{ Auto }

1
1. T : Type
2. x : T
3. L : T List
4. x ↓∈ L
⊢ ↓(x ∈ L)

2
1. T : Type
2. x : T
3. L : T List
4. ↓(x ∈ L)
⊢ x ↓∈ L

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:T  List.    (x  \mdownarrow{}\mmember{}  L  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}(x  \mmember{}  L))


By

---

Latex:
Auto

---

Home Index