---

Step * of Lemma fseg_cons_left

∀[T:Type]. ∀x:T. ∀[L1,L2:T List].  (fseg(T;[x / L1];L2) ⇒ fseg(T;L1;L2))
BY
{ (Unfold `fseg` 0
   THEN Auto
   THEN ExRepD
   THEN InstConcl [⌜L @ [x]⌝]⋅
   THEN Reduce 0
   THEN Auto
   THEN RWO "append_assoc" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}[L1,L2:T  List].    (fseg(T;[x  /  L1];L2)  {}\mRightarrow{}  fseg(T;L1;L2))


By

---

Latex:
(Unfold  `fseg`  0
  THEN  Auto
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}L  @  [x]\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "append\_assoc"  0
  THEN  Auto)

---

Home Index