---

Step * of Lemma cons_before

∀[T:Type]. ∀l:T List. ∀a,x,y:T.  (x before y ∈ [a / l] ⇐⇒ ((x = a ∈ T) ∧ (y ∈ l)) ∨ x before y ∈ l)
BY
{ (Intros THEN ((Unfold `l_before` 0 THEN RWO "member_iff_sublist" 0) THENM RWO "cons_sublist_cons" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l:T  List.  \mforall{}a,x,y:T.    (x  before  y  \mmember{}  [a  /  l]  \mLeftarrow{}{}\mRightarrow{}  ((x  =  a)  \mwedge{}  (y  \mmember{}  l))  \mvee{}  x  before  y  \mmember{}  l)


By

---

Latex:
(Intros
  THEN  ((Unfold  `l\_before`  0  THEN  RWO  "member\_iff\_sublist"  0)  THENM  RWO  "cons\_sublist\_cons"  0)
  THEN  Auto)

---

Home Index