---

Step * 1 of Lemma member_firstn


1. [T] : Type
⊢ ∀n:ℕ. ∀x:T.  ((x ∈ []) ⇐⇒ ∃i:ℕ. ((i < n ∧ i < 0) ∧ (x = ⊥ ∈ T)))
BY
{ TACTIC:(Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}x:T.    ((x  \mmember{}  [])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}.  ((i  <  n  \mwedge{}  i  <  0)  \mwedge{}  (x  =  \mbot{})))


By

---

Latex:
TACTIC:(Auto  THEN  ExRepD  THEN  Auto)

---

Home Index