---

Step * of Lemma subtype-value-type

∀[A,B:Type].  (value-type(A)) supposing (value-type(B) and (A ⊆r B))
BY
{ (ValueTypeAuto THEN Fold `has-value` 0 THEN GenConcl ⌜v = b ∈ B⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (value-type(A))  supposing  (value-type(B)  and  (A  \msubseteq{}r  B))


By

---

Latex:
(ValueTypeAuto  THEN  Fold  `has-value`  0  THEN  GenConcl  \mkleeneopen{}v  =  b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index