---

Step * of Lemma f-subset-empty

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:fset(T)].  (x ⊆ {} ⇐⇒ x = {} ∈ fset(T))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(T)
4. x ⊆ {}
⊢ x = {} ∈ fset(T)

2
1. T : Type
2. eq : EqDecider(T)
3. x : fset(T)
4. x = {} ∈ fset(T)
⊢ x ⊆ {}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:fset(T)].    (x  \msubseteq{}  \{\}  \mLeftarrow{}{}\mRightarrow{}  x  =  \{\})


By

---

Latex:
Auto

---

Home Index