---

Step * 1 of Lemma member-reverse


1. [T] : Type
2. L : T List
3. x : T
4. i : ℕ
5. i < ||rev(L)||
6. x = rev(L)[i] ∈ T
⊢ (x ∈ L)
BY
{ ((RWO "select-reverse" (-1) THENA Auto)
   THEN (RWO "length-reverse" (-2) THENA Auto)
   THEN With ⌜||L|| - 1 - i⌝ (D 0)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  x  :  T
4.  i  :  \mBbbN{}
5.  i  <  ||rev(L)||
6.  x  =  rev(L)[i]
\mvdash{}  (x  \mmember{}  L)


By

---

Latex:
((RWO  "select-reverse"  (-1)  THENA  Auto)
  THEN  (RWO  "length-reverse"  (-2)  THENA  Auto)
  THEN  With  \mkleeneopen{}||L||  -  1  -  i\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index