---

Step * of Lemma inclusion-partial

∀[T:Type]. T ⊆r partial(T) supposing value-type(T)
BY
{ TACTIC:(Auto THEN Assert ⌜∀a:Base. ((a ∈ T) ⇒ (a ∈ base-partial(T)))⌝⋅) }

1
.....assertion..... 
1. T : Type
2. value-type(T)
⊢ ∀a:Base. ((a ∈ T) ⇒ (a ∈ base-partial(T)))

2
1. T : Type
2. value-type(T)
3. ∀a:Base. ((a ∈ T) ⇒ (a ∈ base-partial(T)))
⊢ T ⊆r partial(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  T  \msubseteq{}r  partial(T)  supposing  value-type(T)


By

---

Latex:
TACTIC:(Auto  THEN  Assert  \mkleeneopen{}\mforall{}a:Base.  ((a  \mmember{}  T)  {}\mRightarrow{}  (a  \mmember{}  base-partial(T)))\mkleeneclose{}\mcdot{})

---

Home Index