---

Step * 1 of Lemma tuple2_lemma


1. F : Top@i
⊢ tuple(2;x.F[x]) ~ <F[0], F[1]>
BY
{ (Unfold `tuple` 0 THEN RW (AddrC [1;1;2] UptoC) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Top@i
\mvdash{}  tuple(2;x.F[x])  \msim{}  <F[0],  F[1]>


By

---

Latex:
(Unfold  `tuple`  0  THEN  RW  (AddrC  [1;1;2]  UptoC)  0  THEN  Reduce  0  THEN  Auto)

---

Home Index