---

Step * 2 1 3 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|| = k ∈ ℤ
13. no_repeats(A;L@0)
⊢ (L@0 ∈ L)
BY
{ xxx(RenameVar `x' (-3) THEN InstHyp [⌜x⌝] (-4)⋅ THEN Auto)xxx }

1
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. x : A List
12. ||x|| = k ∈ ℤ
13. no_repeats(A;x)
14. (x ∈ L)
⊢ (x ∈ L)

---

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||  =  k
13.  no\_repeats(A;L@0)
\mvdash{}  (L@0  \mmember{}  L)


By

---

Latex:
xxx(RenameVar  `x'  (-3)  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)xxx

---

Home Index