---

Step * of Lemma l_before_transitivity

∀[T:Type]. ∀l:T List. ∀x,y,z:T.  x before y ∈ l ⇒ y before z ∈ l ⇒ x before z ∈ l supposing no_repeats(T;l)
BY
{ (Unfolds ``l_before`` 0 THEN Auto) }

1
1. [T] : Type
2. l : T List
3. x : T
4. y : T
5. z : T
6. no_repeats(T;l)
7. [x; y] ⊆ l
8. [y; z] ⊆ l
⊢ [x; z] ⊆ l

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}l:T  List.  \mforall{}x,y,z:T.    x  before  y  \mmember{}  l  {}\mRightarrow{}  y  before  z  \mmember{}  l  {}\mRightarrow{}  x  before  z  \mmember{}  l  supposing  no\_repeats(T;l)


By

---

Latex:
(Unfolds  ``l\_before``  0  THEN  Auto)

---

Home Index