---

Step * 1 1 of Lemma combination-decomp

.....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
BY
{ xxx(Auto THEN Lemmaize [-2] THEN InductionOnList THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  n  :  \mBbbN{}\msupplus{}
3.  u  :  A
4.  v  :  A  List
5.  no\_repeats(A;v)  \mwedge{}  (\mneg{}(u  \mmember{}  v))
6.  (||v||  +  1)  =  n
\mvdash{}  v  \mmember{}  \{a:A|  \mneg{}(a  =  u)\}    List


By

---

Latex:
xxx(Auto  THEN  Lemmaize  [-2]  THEN  InductionOnList  THEN  Auto)xxx

---

Home Index