---

Step * 1 1 of Lemma stream-extensionality


1. A : Type
2. x : stream(A)
3. y : stream(A)
4. ∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)
5. x1 : stream(A)
6. y1 : stream(A)
7. ∀n:ℕ. (s-nth(n;x1) = s-nth(n;y1) ∈ A)
8. x1 ~ s-hd(x1).s-tl(x1)
9. y1 ~ s-hd(y1).s-tl(y1)
⊢ (s-nth(0;s-hd(x1).s-tl(x1)) = s-nth(0;s-hd(y1).s-tl(y1)) ∈ A)
⇒ (s-hd(s-hd(x1).s-tl(x1)) = s-hd(s-hd(y1).s-tl(y1)) ∈ A)
BY
{ (RecUnfold `s-nth` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  x  :  stream(A)
3.  y  :  stream(A)
4.  \mforall{}n:\mBbbN{}.  (s-nth(n;x)  =  s-nth(n;y))
5.  x1  :  stream(A)
6.  y1  :  stream(A)
7.  \mforall{}n:\mBbbN{}.  (s-nth(n;x1)  =  s-nth(n;y1))
8.  x1  \msim{}  s-hd(x1).s-tl(x1)
9.  y1  \msim{}  s-hd(y1).s-tl(y1)
\mvdash{}  (s-nth(0;s-hd(x1).s-tl(x1))  =  s-nth(0;s-hd(y1).s-tl(y1)))
{}\mRightarrow{}  (s-hd(s-hd(x1).s-tl(x1))  =  s-hd(s-hd(y1).s-tl(y1)))


By

---

Latex:
(RecUnfold  `s-nth`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index