---

Step * 1 of Lemma subtype-mono


1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. ∀a:B. ∀b:Base.  (is-above(B;a;b) ⇒ (a = b ∈ B))
5. a : A@i
6. ∀b:Base. (is-above(B;a;b) ⇒ (a = b ∈ B))
7. b : Base@i
8. is-above(A;a;b)@i
9. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
⊢ is-above(B;a;b)
BY
{ (D 3 THEN FLemma `is-above-subtype` [3;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  strong-subtype(A;B)
4.  \mforall{}a:B.  \mforall{}b:Base.    (is-above(B;a;b)  {}\mRightarrow{}  (a  =  b))
5.  a  :  A@i
6.  \mforall{}b:Base.  (is-above(B;a;b)  {}\mRightarrow{}  (a  =  b))
7.  b  :  Base@i
8.  is-above(A;a;b)@i
9.  \mforall{}b:B.  \mforall{}a:A.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
\mvdash{}  is-above(B;a;b)


By

---

Latex:
(D  3  THEN  FLemma  `is-above-subtype`  [3;-2]  THEN  Auto)

---

Home Index