---

Step * 2 of Lemma member-reverse


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index