---

Step * of Lemma top-subtype-function

∀[A,B:Type].  Top ⊆r (A ⟶ B) supposing ¬A
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. ¬A
4. x : Top@i
⊢ x ∈ A ⟶ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    Top  \msubseteq{}r  (A  {}\mrightarrow{}  B)  supposing  \mneg{}A


By

---

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

---

Home Index