---

Step * 1 of Lemma combination-decomp


1. A : Type
2. n : ℕ+
3. u : A
4. v : A List
5. no_repeats(A;[u / v])
6. (||v|| + 1) = n ∈ ℤ
⊢ v ∈ Combination(n - 1;{a:A| ¬(a = u ∈ A)} )
BY
{ xxx((RWO "no_repeats_cons" (-2) THENA Auto) THEN Assert ⌜v ∈ {a:A| ¬(a = u ∈ A)}  List⌝⋅)xxx }

1
.....assertion..... 
1. A : Type
2. n : ℕ+
3. u : A
4. v : A List
5. no_repeats(A;v) ∧ (¬(u ∈ v))
6. (||v|| + 1) = n ∈ ℤ
⊢ v ∈ {a:A| ¬(a = u ∈ A)}  List

2
1. A : Type
2. n : ℕ+
3. u : A
4. v : A List
5. no_repeats(A;v) ∧ (¬(u ∈ v))
6. (||v|| + 1) = n ∈ ℤ
7. v ∈ {a:A| ¬(a = u ∈ A)}  List
⊢ v ∈ Combination(n - 1;{a:A| ¬(a = u ∈ A)} )

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbN{}\msupplus{}
3.  u  :  A
4.  v  :  A  List
5.  no\_repeats(A;[u  /  v])
6.  (||v||  +  1)  =  n
\mvdash{}  v  \mmember{}  Combination(n  -  1;\{a:A|  \mneg{}(a  =  u)\}  )


By

---

Latex:
xxx((RWO  "no\_repeats\_cons"  (-2)  THENA  Auto)  THEN  Assert  \mkleeneopen{}v  \mmember{}  \{a:A|  \mneg{}(a  =  u)\}    List\mkleeneclose{}\mcdot{})xxx

---

Home Index