---

Step * 2 of Lemma free-vs-inc_wf


1. S : Type
2. K : RngSig
3. s : S
4. <s> = <s> ∈ basic-formal-sum(K;S)
⊢ basic-formal-sum(K;S) ⊆r Point(free-vs(K;S))
BY
{ (RepUR ``vs-point free-vs mk-vs`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  RngSig
3.  s  :  S
4.  <s>  =  <s>
\mvdash{}  basic-formal-sum(K;S)  \msubseteq{}r  Point(free-vs(K;S))


By

---

Latex:
(RepUR  ``vs-point  free-vs  mk-vs``  0  THEN  ProveWfLemma)

---

Home Index