---

Step * 2 1 1 of Lemma combinations-list


1. A : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
5. c : ℕ
6. Combination(k;A) ~ ℕc
7. L : Combination(k;A) List
8. no_repeats(Combination(k;A);L)
9. ||L|| = c ∈ ℤ
10. ∀x:Combination(k;A). (x ∈ L)
11. L@0 : A List
12. (L@0 ∈ L)
⊢ ||L@0|| = k ∈ ℤ
BY
{ xxx(RepeatFor 2 (D -1) THEN HypSubst' (-1) 0 THEN Auto THEN (GenConclAtAddr [2;1] THEN D -2) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbN{}
3.  A  \msim{}  \mBbbN{}n
4.  k  :  \mBbbN{}
5.  c  :  \mBbbN{}
6.  Combination(k;A)  \msim{}  \mBbbN{}c
7.  L  :  Combination(k;A)  List
8.  no\_repeats(Combination(k;A);L)
9.  ||L||  =  c
10.  \mforall{}x:Combination(k;A).  (x  \mmember{}  L)
11.  L@0  :  A  List
12.  (L@0  \mmember{}  L)
\mvdash{}  ||L@0||  =  k


By

---

Latex:
xxx(RepeatFor  2  (D  -1)
        THEN  HypSubst'  (-1)  0
        THEN  Auto
        THEN  (GenConclAtAddr  [2;1]  THEN  D  -2)
        THEN  Auto)xxx

---

Home Index