---

Step * of Lemma fset-size-proper-subset

∀[T:Type]. ∀eq:EqDecider(T). ∀x,ys:fset(T).  (ys ⊆≠ x ⇒ ||ys|| < ||x||)
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(T)
4. ys : fset(T)
5. ys ⊆≠ x
⊢ ||ys|| < ||x||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x,ys:fset(T).    (ys  \msubseteq{}\mneq{}  x  {}\mRightarrow{}  ||ys||  <  ||x||)


By

---

Latex:
Auto

---

Home Index