---

Step * of Lemma injections-combinations

∀n:ℕ. ∀[T:Type]. ℕn →⟶ T ~ Combination(n;T)
BY
{ TACTIC:Auto }

1
1. n : ℕ
2. [T] : Type
⊢ ℕn →⟶ T ~ Combination(n;T)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}[T:Type].  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  T  \msim{}  Combination(n;T)


By

---

Latex:
TACTIC:Auto

---

Home Index