---

Step * of Lemma strong-subtype-member

∀[A,B:Type]. ∀[b:B]. ∀[a:A].  {b ∈ A supposing b = a ∈ B} supposing strong-subtype(A;B)
BY
{ (Unfold `guard` 0 THEN Auto THEN (All (Unfold `strong-subtype`)) THEN ExRepD THEN TrySubsume) }

1
1. A : Type
2. B : Type
3. b : B
4. a : A
5. A ⊆r B
6. {b:B| ∃a:A. (b = a ∈ B)}  ⊆r A
7. b = a ∈ B
⊢ b ∈ A

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:B].  \mforall{}[a:A].    \{b  \mmember{}  A  supposing  b  =  a\}  supposing  strong-subtype(A;B)


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto  THEN  (All  (Unfold  `strong-subtype`))  THEN  ExRepD  THEN  TrySubsume)

---

Home Index