---

Step * of Lemma subtype-mono

∀[A,B:Type].  (mono(A)) supposing (mono(B) and strong-subtype(A;B))
BY
{ (Auto
   THEN RepeatFor 4 (ParallelLast)
   THEN (FLemma `strong-subtype-implies` [3] THENA Auto)
   THEN Try ((Symmetry THEN Complete (Auto)))) }

1
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)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (mono(A))  supposing  (mono(B)  and  strong-subtype(A;B))


By

---

Latex:
(Auto
  THEN  RepeatFor  4  (ParallelLast)
  THEN  (FLemma  `strong-subtype-implies`  [3]  THENA  Auto)
  THEN  Try  ((Symmetry  THEN  Complete  (Auto))))

---

Home Index