Step * 1 of Lemma assert-deq-member


1. [A] Type
2. eq EqDecider(A)
⊢ ∀x:A. (False ⇐⇒ (x ∈ []))
BY
(RepUR  ``deq-member`` 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