Step
*
of Lemma
member-reverse
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ rev(L))
⇐⇒ (x ∈ L))
BY
{ (Auto THEN RepeatFor 2 (D -1)) }
1
1. [T] : Type
2. L : T List
3. x : T
4. i : ℕ
5. i < ||rev(L)||
6. x = rev(L)[i] ∈ T
⊢ (x ∈ L)
2
1. [T] : Type
2. L : T List
3. x : T
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
⊢ (x ∈ rev(L))
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}L:T List. \mforall{}x:T. ((x \mmember{} rev(L)) \mLeftarrow{}{}\mRightarrow{} (x \mmember{} L))
By
Latex:
(Auto THEN RepeatFor 2 (D -1))
Home
Index