---

Step * of Lemma subtype-valueall-type

∀[A,B:Type].  (valueall-type(A)) supposing (valueall-type(B) and (A ⊆r B))
BY
{ (ValueTypeAuto THEN Fold `has-value` 0 THEN Fold `has-valueall` 0) }

1
1. A : Type
2. B : Type
3. A ⊆r B
4. valueall-type(B)
5. x : Base
6. x ∈ A
7. v : A
⊢ has-valueall(v)

---

Latex:

---

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


By

---

Latex:
(ValueTypeAuto  THEN  Fold  `has-value`  0  THEN  Fold  `has-valueall`  0)

---

Home Index