---

Step * 1 of Lemma not-member-mFOL-sequent-freevars


1. v : ℤ
⊢ ∀v1:ℤ List. (¬(v ∈ v1) ⇐⇒ (¬(v ∈ v1)) ∧ True)
BY
{ Auto }

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
\mvdash{}  \mforall{}v1:\mBbbZ{}  List.  (\mneg{}(v  \mmember{}  v1)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(v  \mmember{}  v1))  \mwedge{}  True)


By

---

Latex:
Auto

---

Home Index