---

Step * 1 1 1 of Lemma stream-bijection


1. A : Type
2. a1 : stream(A)
3. a2 : stream(A)
4. (λn.s-nth(n;a1)) = (λn.s-nth(n;a2)) ∈ (ℕ ⟶ A)
5. n : ℕ
⊢ s-nth(n;a1) = s-nth(n;a2) ∈ A
BY
{ (ApFunToHypEquands `Z' ⌜Z n⌝ ⌜A⌝ (-2)⋅ THEN Reduce (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  a1  :  stream(A)
3.  a2  :  stream(A)
4.  (\mlambda{}n.s-nth(n;a1))  =  (\mlambda{}n.s-nth(n;a2))
5.  n  :  \mBbbN{}
\mvdash{}  s-nth(n;a1)  =  s-nth(n;a2)


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}Z  n\mkleeneclose{}  \mkleeneopen{}A\mkleeneclose{}  (-2)\mcdot{}  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index