---

Step * of Lemma eq-0-in-relative-free-vs

∀[K:CRng]. ∀[S,T:Type].
  ∀[x:Point(free-vs(K;S))]. x = 0 ∈ Point(relative-free-vs(K;S;T)) supposing ↓fs-in-subtype(K;S;T;x) 
  supposing strong-subtype(T;S)
BY
{ (Unfold `relative-free-vs` 0 THEN Auto THEN BLemma `eq-0-in-vs-quotient` THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[S,T:Type].
    \mforall{}[x:Point(free-vs(K;S))].  x  =  0  supposing  \mdownarrow{}fs-in-subtype(K;S;T;x)  supposing  strong-subtype(T;S)


By

---

Latex:
(Unfold  `relative-free-vs`  0  THEN  Auto  THEN  BLemma  `eq-0-in-vs-quotient`  THEN  EAuto  1)

---

Home Index