---

Step * of Lemma shorten-tuple-simplify

∀[p:Top × Top × Top]. (fst(shorten-tuple(p;1)) ~ fst(snd(p)))
BY
{ ((D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:Top  \mtimes{}  Top  \mtimes{}  Top].  (fst(shorten-tuple(p;1))  \msim{}  fst(snd(p)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  Reduce  0  THEN  Auto)

---

Home Index