---

Step * 1 of Lemma distinct_iff_counts_le_one


1. s : DSet
⊢ True ⇐⇒ ∀x:|s|. (0 ≤ 1)
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  s  :  DSet
\mvdash{}  True  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  (0  \mleq{}  1)


By

---

Latex:
TACTIC:Auto

---

Home Index