---

Step * of Lemma fseg_append

∀[T:Type]. ∀l1,l2,l3:T List.  (fseg(T;l1;l2) ⇒ fseg(T;l1;l3 @ l2))
BY
{ (Unfold `fseg` 0
   THEN Auto
   THEN ExRepD
   THEN ((InstConcl [l3 @ L])⋅ THENM WeakSubstFor l2 0⋅ THENM RWO "append_assoc" 0)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `fseg`  0
  THEN  Auto
  THEN  ExRepD
  THEN  ((InstConcl  [l3  @  L])\mcdot{}  THENM  WeakSubstFor  l2  0\mcdot{}  THENM  RWO  "append\_assoc"  0)
  THEN  Auto)

---

Home Index