---

Step * 1 of Lemma tuple1_lemma


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

---

Latex:

---

Latex:

1.  F  :  Top
\mvdash{}  tuple(1;x.F[x])  \msim{}  F[0]


By

---

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

---

Home Index