---

Step * of Lemma b-union-base-equality

∀A:Type. ∀a,b:Base.  ((a = b ∈ (Base ⋃ A)) ⇒ (b ∈ A) ⇒ (a = b ∈ A))
BY
{ (InstLemma `strong-subtype-union-base` []⋅
   THEN ParallelLast'
   THEN D -1
   THEN (FLemma `strong-subtype-implies` [-1] THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}a,b:Base.    ((a  =  b)  {}\mRightarrow{}  (b  \mmember{}  A)  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(InstLemma  `strong-subtype-union-base`  []\mcdot{}
  THEN  ParallelLast'
  THEN  D  -1
  THEN  (FLemma  `strong-subtype-implies`  [-1]  THENA  Auto))

---

Home Index