---

Step * of Lemma sq_stable__fseg

∀[T:Type]. ∀l1,l2:T List.  SqStable(fseg(T;l1;l2))
BY
{ (Unfold `fseg` 0
   THEN Auto
   THEN Unfold `sq_stable` 0
   THEN Auto
   THEN (InstConcl [⌜firstn(||l2|| - ||l1||;l2)⌝]⋅ THENA Auto)
   THEN SquashExRepD
   THEN HypSubst' (-1) 0
   THEN Subst' ||L @ l1|| - ||l1|| ~ ||L|| 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN (RWO "firstn_append" 0 THEN Auto)
   THEN RWO "firstn_all" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `fseg`  0
  THEN  Auto
  THEN  Unfold  `sq\_stable`  0
  THEN  Auto
  THEN  (InstConcl  [\mkleeneopen{}firstn(||l2||  -  ||l1||;l2)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  HypSubst'  (-1)  0
  THEN  Subst'  ||L  @  l1||  -  ||l1||  \msim{}  ||L||  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  (RWO  "firstn\_append"  0  THEN  Auto)
  THEN  RWO  "firstn\_all"  0
  THEN  Auto)

---

Home Index