---

Step * of Lemma member-firstn

∀[T:Type]. ∀L:T List. ∀n:ℕ||L|| + 1. ∀x:T.  ((x ∈ firstn(n;L)) ⇐⇒ ∃i:ℕn. (x = L[i] ∈ T))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `member_firstn` [⌜T⌝;⌜L⌝;⌜n⌝;⌜x⌝]⋅
   THEN Auto
   THEN Try (BackThruSomeHyp)
   THEN OnSomeHyp ParallelExists
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}n:\mBbbN{}||L||  +  1.  \mforall{}x:T.    ((x  \mmember{}  firstn(n;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (x  =  L[i]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `member\_firstn`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (BackThruSomeHyp)
  THEN  OnSomeHyp  ParallelExists
  THEN  Auto)

---

Home Index