---

Step * of Lemma fseg_transitivity

∀[T:Type]. ∀l1,l2,l3:T List.  (fseg(T;l1;l2) ⇒ fseg(T;l2;l3) ⇒ fseg(T;l1;l3))
BY
{ ((((Unfold `fseg` 0 THEN Auto') THEN D -1) THEN ExRepD) THEN WeakSubstFor l3 0 THEN WeakSubstFor l2 0) }

1
1. [T] : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. L1 : T List
6. l2 = (L1 @ l1) ∈ (T List)
7. L : T List
8. l3 = (L @ l2) ∈ (T List)
⊢ ∃L@0:T List. ((L @ L1 @ l1) = (L@0 @ l1) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2,l3:T  List.    (fseg(T;l1;l2)  {}\mRightarrow{}  fseg(T;l2;l3)  {}\mRightarrow{}  fseg(T;l1;l3))


By

---

Latex:
((((Unfold  `fseg`  0  THEN  Auto')  THEN  D  -1)  THEN  ExRepD)
  THEN  WeakSubstFor  l3  0
  THEN  WeakSubstFor  l2  0)

---

Home Index