---

Step * 1 1 of Lemma injections-combinations

.....assertion..... 
1. n : ℕ
2. [T] : Type
⊢ λf.mklist(n;f) ∈ ℕn →⟶ T ⟶ Combination(n;T)
BY
{ TACTIC:(Auto
          THEN D -1
          THEN MemTypeCD
          THEN Auto
          THEN RWW "mklist_length" 0
          THEN Auto
          THEN RepeatFor 5 ((D 0 THENA Auto))) }

1
1. n : ℕ
2. T : Type
3. f : ℕn ⟶ T
4. Inj(ℕn;T;f)
5. i : ℕ
6. j : ℕ
7. i < ||mklist(n;f)||
8. j < ||mklist(n;f)||
9. ¬(i = j ∈ ℕ)
⊢ ¬(mklist(n;f)[i] = mklist(n;f)[j] ∈ T)

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  [T]  :  Type
\mvdash{}  \mlambda{}f.mklist(n;f)  \mmember{}  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  T  {}\mrightarrow{}  Combination(n;T)


By

---

Latex:
TACTIC:(Auto
                THEN  D  -1
                THEN  MemTypeCD
                THEN  Auto
                THEN  RWW  "mklist\_length"  0
                THEN  Auto
                THEN  RepeatFor  5  ((D  0  THENA  Auto)))

---

Home Index