---

Step * of Lemma nil_member-variant

∀[T,A:Type].  ∀x:T. (x ∈ []) ⇐⇒ False supposing A ⊆r T
BY
{ xxx(Unfold `l_member` 0 THEN Auto THEN All Reduce THEN ExRepD THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].    \mforall{}x:T.  (x  \mmember{}  [])  \mLeftarrow{}{}\mRightarrow{}  False  supposing  A  \msubseteq{}r  T


By

---

Latex:
xxx(Unfold  `l\_member`  0  THEN  Auto  THEN  All  Reduce  THEN  ExRepD  THEN  Auto)xxx

---

Home Index