---

Step * of Lemma sub-free-dim-1

∀[K:CRng]. ∀[S,T:Type].
  (∀s:T. ∀x:Point(sub-free-vs(K;S;T)).  (↓∃k:|K|. (x = {<k, s>} ∈ Point(sub-free-vs(K;S;T))))) supposing 
     ((∀x,y:T.  (x = y ∈ T)) and 
     strong-subtype(T;S))
BY
{ (Auto
   THEN RepUR ``vs-point sub-free-vs sub-vs mk-vs`` -1
   THEN Fold `vs-point` (-1)
   THEN D -1
   THEN DupHyp (-1)
   THEN RepeatFor 3 (D -1)
   THEN RepUR ``vs-point sub-free-vs sub-vs mk-vs`` 0
   THEN Fold `vs-point` 0) }

1
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. ∀x,y:T.  (x = y ∈ T)
6. s : T
7. x : Point(free-vs(K;S))
8. fs-in-subtype(K;S;T;x)
9. b : basic-formal-sum(K;S)
10. x = b ∈ formal-sum(K;S)
11. bfs-predicate(K;S;p.snd(p) ∈ T;b)
⊢ ↓∃k:|K|. (x = {<k, s>} ∈ {f:Point(free-vs(K;S))| fs-in-subtype(K;S;T;f)} )

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[S,T:Type].
    (\mforall{}s:T.  \mforall{}x:Point(sub-free-vs(K;S;T)).    (\mdownarrow{}\mexists{}k:|K|.  (x  =  \{<k,  s>\})))  supposing 
          ((\mforall{}x,y:T.    (x  =  y))  and 
          strong-subtype(T;S))


By

---

Latex:
(Auto
  THEN  RepUR  ``vs-point  sub-free-vs  sub-vs  mk-vs``  -1
  THEN  Fold  `vs-point`  (-1)
  THEN  D  -1
  THEN  DupHyp  (-1)
  THEN  RepeatFor  3  (D  -1)
  THEN  RepUR  ``vs-point  sub-free-vs  sub-vs  mk-vs``  0
  THEN  Fold  `vs-point`  0)

---

Home Index