---

Step * of Lemma before-reverse

∀[T:Type]. ∀L:T List. ∀x,y:T.  (x before y ∈ rev(L) ⇐⇒ y before x ∈ L)
BY
{ TACTIC:(InductionOnList THEN Reduce 0) }

1
1. [T] : Type
⊢ ∀x,y:T.  (x before y ∈ [] ⇐⇒ y before x ∈ [])

2
1. [T] : Type
2. u : T@i
3. v : T List@i
4. ∀x,y:T.  (x before y ∈ rev(v) ⇐⇒ y before x ∈ v)
⊢ ∀x,y:T.  (x before y ∈ rev(v) @ [u] ⇐⇒ y before x ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x,y:T.    (x  before  y  \mmember{}  rev(L)  \mLeftarrow{}{}\mRightarrow{}  y  before  x  \mmember{}  L)


By

---

Latex:
TACTIC:(InductionOnList  THEN  Reduce  0)

---

Home Index