---

Step * of Lemma free-vs-inc_wf

∀[S:Type]. ∀[K:RngSig]. ∀[s:S].  (<s> ∈ Point(free-vs(K;S)))
BY
{ (Auto THEN SubsumeC ⌜basic-formal-sum(K;S)⌝⋅) }

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

2
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))

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[s:S].    (<s>  \mmember{}  Point(free-vs(K;S)))


By

---

Latex:
(Auto  THEN  SubsumeC  \mkleeneopen{}basic-formal-sum(K;S)\mkleeneclose{}\mcdot{})

---

Home Index