---

Step * of Lemma strong-subtype-union-base

∀[A:Type]. (strong-subtype(A;A ⋃ Base) ∧ strong-subtype(A;Base ⋃ A))
BY
{ Auto }

1
1. A : Type
⊢ strong-subtype(A;A ⋃ Base)

2
1. A : Type
2. strong-subtype(A;A ⋃ Base)
⊢ strong-subtype(A;Base ⋃ A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  (strong-subtype(A;A  \mcup{}  Base)  \mwedge{}  strong-subtype(A;Base  \mcup{}  A))


By

---

Latex:
Auto

---

Home Index