---

Step * of Lemma stream-extensionality

∀[A:Type]. ∀[x,y:stream(A)].  x = y ∈ stream(A) supposing ∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)
BY
{ (Auto THEN InstLemma `stream-coinduction` [⌜A⌝;⌜λ2x y.∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)⌝]⋅ THEN Auto) }

1
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)
⊢ s-hd(x1) = s-hd(y1) ∈ A

2
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. s-hd(x1) = s-hd(y1) ∈ A
9. n : ℕ
⊢ s-nth(n;s-tl(x1)) = s-nth(n;s-tl(y1)) ∈ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[x,y:stream(A)].    x  =  y  supposing  \mforall{}n:\mBbbN{}.  (s-nth(n;x)  =  s-nth(n;y))


By

---

Latex:
(Auto  THEN  InstLemma  `stream-coinduction`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.\mforall{}n:\mBbbN{}.  (s-nth(n;x)  =  s-nth(n;y))\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index