---

Step * 1 of Lemma b-union-base-equality


1. A : Type
2. strong-subtype(A;A ⋃ Base)
3. strong-subtype(A;Base ⋃ A)
4. ∀b:Base ⋃ A. ∀a:A.  ((b = a ∈ (Base ⋃ A)) ⇒ (b = a ∈ A))
⊢ ∀a,b:Base.  ((a = b ∈ (Base ⋃ A)) ⇒ (b ∈ A) ⇒ (a = b ∈ A))
BY
{ (Intros THEN FHyp 4 [-2] THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  strong-subtype(A;A  \mcup{}  Base)
3.  strong-subtype(A;Base  \mcup{}  A)
4.  \mforall{}b:Base  \mcup{}  A.  \mforall{}a:A.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
\mvdash{}  \mforall{}a,b:Base.    ((a  =  b)  {}\mRightarrow{}  (b  \mmember{}  A)  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(Intros  THEN  FHyp  4  [-2]  THEN  Auto)

---

Home Index