---

Step * 1 1 of Lemma data-stream-cons

.....wf..... 
1. L : Top List
2. a : Top
3. P : Top
⊢ ||[a / L]|| ∈ ℕ+
BY
{ (Auto THEN Auto') }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  Top  List
2.  a  :  Top
3.  P  :  Top
\mvdash{}  ||[a  /  L]||  \mmember{}  \mBbbN{}\msupplus{}


By

---

Latex:
(Auto  THEN  Auto')

---

Home Index