---

Step * 1 of Lemma free-vs-inc_wf


1. S : Type
2. K : RngSig
3. s : S
⊢ <s> ∈ basic-formal-sum(K;S)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  RngSig
3.  s  :  S
\mvdash{}  <s>  \mmember{}  basic-formal-sum(K;S)


By

---

Latex:
ProveWfLemma

---

Home Index