---

Step * 1 1 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 < n
8. j < n
9. (f i) = (f j) ∈ T
⊢ i = j ∈ ℕ
BY
{ (BackThruSomeHyp' THEN Auto) }

---

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  <  n
8.  j  <  n
9.  (f  i)  =  (f  j)
\mvdash{}  i  =  j


By

---

Latex:
(BackThruSomeHyp'  THEN  Auto)

---

Home Index