---

Step * of Lemma strong-subtype-union

∀[A,B,C,D:Type].  (strong-subtype(A + B;C + D)) supposing (strong-subtype(B;D) and strong-subtype(A;C))
BY
{ (Auto
   THEN (FLemma `strong-subtype-implies` [5] THENA Auto)
   THEN (FLemma `strong-subtype-implies` [6] THENA Auto)
   THEN D 5
   THEN D 7
   THEN (D 0 THEN Try (Complete (Auto)))
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (D -3 THEN Auto)
   THEN D -2
   THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. A ⊆r C
6. {b:C| ∃a:A. (b = a ∈ C)}  ⊆r A
7. B ⊆r D
8. {b:D| ∃a:B. (b = a ∈ D)}  ⊆r B
9. ∀b:C. ∀a:A.  ((b = a ∈ C) ⇒ (b = a ∈ A))
10. ∀b:D. ∀a:B.  ((b = a ∈ D) ⇒ (b = a ∈ B))
11. (A + B) ⊆r (C + D)
12. x1 : C
13. x : A
14. x1 = x ∈ C
⊢ x1 ∈ A

2
1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. A ⊆r C
6. {b:C| ∃a:A. (b = a ∈ C)}  ⊆r A
7. B ⊆r D
8. {b:D| ∃a:B. (b = a ∈ D)}  ⊆r B
9. ∀b:C. ∀a:A.  ((b = a ∈ C) ⇒ (b = a ∈ A))
10. ∀b:D. ∀a:B.  ((b = a ∈ D) ⇒ (b = a ∈ B))
11. (A + B) ⊆r (C + D)
12. y : D
13. y1 : B
14. y = y1 ∈ D
⊢ y ∈ B

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (FLemma  `strong-subtype-implies`  [5]  THENA  Auto)
  THEN  (FLemma  `strong-subtype-implies`  [6]  THENA  Auto)
  THEN  D  5
  THEN  D  7
  THEN  (D  0  THEN  Try  (Complete  (Auto)))
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (D  -3  THEN  Auto)
  THEN  D  -2
  THEN  Auto)

---

Home Index