---

Step * of Lemma subtype_imp-type

∀[A,B:Type].  (B ⊆r imp-type(A;B))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. x : B
⊢ x ∈ imp-type(A;B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (B  \msubseteq{}r  imp-type(A;B))


By

---

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

---

Home Index