---

Step * 1 1 1 of Lemma injections-combinations


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)
BY
{ ((RWW "mklist_length" (-3) THENA Auto)
   THEN (RWW "mklist_length" (-2) THENA Auto)
   THEN TACTIC:(RWO "mklist_select" 0 THEN Auto)) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  T  :  Type
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  Inj(\mBbbN{}n;T;f)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||mklist(n;f)||
8.  j  <  ||mklist(n;f)||
9.  \mneg{}(i  =  j)
\mvdash{}  \mneg{}(mklist(n;f)[i]  =  mklist(n;f)[j])


By

---

Latex:
((RWW  "mklist\_length"  (-3)  THENA  Auto)
  THEN  (RWW  "mklist\_length"  (-2)  THENA  Auto)
  THEN  TACTIC:(RWO  "mklist\_select"  0  THEN  Auto))

---

Home Index