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