---

Step * 1 of Lemma assert-deq-member


1. [A] : Type
2. eq : EqDecider(A)
⊢ ∀x:A. (False ⇐⇒ (x ∈ []))
BY
{ (RepUR  ``deq-member`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  eq  :  EqDecider(A)
\mvdash{}  \mforall{}x:A.  (False  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  []))


By

---

Latex:
(RepUR    ``deq-member``  0  THEN  Auto)

---

Home Index