---

Step * of Lemma seq-comp-truncate

∀[T:Type]. ∀[s:sequence(T)]. ∀[f,n:Top].  (f o seq-truncate(s;n) ~ seq-truncate(f o s;n))
BY
{ (Intros THEN UseWitness ⌜Ax⌝⋅ THEN D 2 THEN RepUR ``seq-truncate seq-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].  \mforall{}[f,n:Top].    (f  o  seq-truncate(s;n)  \msim{}  seq-truncate(f  o  s;n))


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  D  2  THEN  RepUR  ``seq-truncate  seq-comp``  0  THEN  Auto)

---

Home Index