---

Step * of Lemma subtype-approx-type

∀[T:Type]. T ⊆r approx-type(T) supposing mono(T) ∨ (T ⊆r Base)
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. T : Type
2. mono(T) ∨ (T ⊆r Base)
3. x : T
⊢ x ∈ approx-type(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  T  \msubseteq{}r  approx-type(T)  supposing  mono(T)  \mvee{}  (T  \msubseteq{}r  Base)


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index