---

Step * of Lemma append-tuple-simplify

∀[p:Top × Top]. (fst(snd(let x,y = p in <x, y, ⋅>)) ~ snd(p))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:Top  \mtimes{}  Top].  (fst(snd(let  x,y  =  p  in  <x,  y,  \mcdot{}>))  \msim{}  snd(p))


By

---

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

---

Home Index