---

Step * 1 1 1 of Lemma count-unordered-combinations

.....antecedent..... 
1. n : ℕ
2. m : ℕ
3. n < m
4. L : ℕn List
5. no_repeats(ℕn;L)
6. ||L|| = m ∈ ℤ
⊢ Inj(ℕm;ℕn;λi.L[i])
BY
{ (D 0 THEN Reduce 0 THEN Auto) }

1
1. n : ℕ
2. m : ℕ
3. n < m
4. L : ℕn List
5. no_repeats(ℕn;L)
6. ||L|| = m ∈ ℤ
7. a1 : ℕm
8. a2 : ℕm
9. L[a1] = L[a2] ∈ ℕn
⊢ a1 = a2 ∈ ℕm

---

Latex:

---

Latex:
.....antecedent..... 
1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  <  m
4.  L  :  \mBbbN{}n  List
5.  no\_repeats(\mBbbN{}n;L)
6.  ||L||  =  m
\mvdash{}  Inj(\mBbbN{}m;\mBbbN{}n;\mlambda{}i.L[i])


By

---

Latex:
(D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index