---

Step * of Lemma member_tl

∀[T:Type]. ∀as:T List. ∀x:T.  (x ∈ tl(as)) ⇒ (x ∈ as) supposing 0 < ||as||
BY
{ ((Auto THEN ParallelOp (-1))
   THEN ExRepD
   THEN RWO "length_tl" (-2)
   THEN Auto'
   THEN InstConcl [i + 1]
   THEN Auto
   THEN AllHyps (RWO "select_tl")
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as:T  List.  \mforall{}x:T.    (x  \mmember{}  tl(as))  {}\mRightarrow{}  (x  \mmember{}  as)  supposing  0  <  ||as||


By

---

Latex:
((Auto  THEN  ParallelOp  (-1))
  THEN  ExRepD
  THEN  RWO  "length\_tl"  (-2)
  THEN  Auto'
  THEN  InstConcl  [i  +  1]
  THEN  Auto
  THEN  AllHyps  (RWO  "select\_tl")
  THEN  Auto)

---

Home Index