---

Step * of Lemma strong-subtype-fset-member-type

∀[A,B:Type]. ∀[eq:EqDecider(B)].  ∀[s:fset(A)]. ∀[x:B].  x ∈ A supposing x ∈ s supposing strong-subtype(A;B)
BY
{ (TACTIC:BasicUniformUnivCD Auto THEN Assert ⌜s ∈ fset(B)⌝⋅ THEN Auto) }

1
1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. strong-subtype(A;B)
5. s : fset(A)
6. x : B
7. s ∈ fset(B)
8. x ∈ s
⊢ x ∈ A

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:EqDecider(B)].
    \mforall{}[s:fset(A)].  \mforall{}[x:B].    x  \mmember{}  A  supposing  x  \mmember{}  s  supposing  strong-subtype(A;B)


By

---

Latex:
(TACTIC:BasicUniformUnivCD  Auto  THEN  Assert  \mkleeneopen{}s  \mmember{}  fset(B)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index