---

Step * of Lemma seq-append0

∀[n:ℕ]. ∀[s,t:Top].  (seq-append(n;0;s;t) ~ seq-normalize(n;s))
BY
{ (RepUR ``seq-append seq-normalize`` 0
   THEN (UnivCD THENA Auto)
   THEN EqCD
   THEN SqEqualBase
   THEN BLemma `less_sqequal`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s,t:Top].    (seq-append(n;0;s;t)  \msim{}  seq-normalize(n;s))


By

---

Latex:
(RepUR  ``seq-append  seq-normalize``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  EqCD
  THEN  SqEqualBase
  THEN  BLemma  `less\_sqequal`
  THEN  Auto)

---

Home Index