---

Step * 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)
⊢ s-hd(x1) = s-hd(y1) ∈ A
BY
{ ((InstHyp [⌜0⌝] (-1)⋅ THEN Auto)
   THEN MoveToConcl (-1)
   THEN ((InstLemma `stream-decomp` [⌜x1⌝]⋅ THENM HypSubst'(-1) 0) THENA (DoSubsume THEN Auto))
   THEN ((InstLemma `stream-decomp` [⌜y1⌝]⋅ THENM HypSubst'(-1) 0) THENA (DoSubsume 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)
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)

---

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))
\mvdash{}  s-hd(x1)  =  s-hd(y1)


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((InstLemma  `stream-decomp`  [\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}  THENM  HypSubst'(-1)  0)  THENA  (DoSubsume  THEN  Auto))
  THEN  ((InstLemma  `stream-decomp`  [\mkleeneopen{}y1\mkleeneclose{}]\mcdot{}  THENM  HypSubst'(-1)  0)  THENA  (DoSubsume  THEN  Auto)))

---

Home Index