---

Step * 1 of Lemma s-nth_wf


1. A : Type
2. n : ℤ
3. s : stream(A)
⊢ let a,s' = s 
  in a ∈ A
BY
{ (Fold `pi1` 0 THEN Fold `s-hd` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbZ{}
3.  s  :  stream(A)
\mvdash{}  let  a,s'  =  s 
    in  a  \mmember{}  A


By

---

Latex:
(Fold  `pi1`  0  THEN  Fold  `s-hd`  0  THEN  Auto)

---

Home Index