---

Step * 1 of Lemma no-repeats-pairwise


1. [T] : Type
2. L : T List@i
3. [P] : {x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ'
4. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. ∀x,y:{x:T| (x ∈ L)} .  P[x;y] supposing ¬(x = y ∈ T)@i'
⊢ ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]
BY
{ (Auto THEN RepeatFor 2 ((BackThruSomeHyp THEN Auto'))) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List@i
3.  [P]  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}'
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
5.  \mforall{}x,y:\{x:T|  (x  \mmember{}  L)\}  .    P[x;y]  supposing  \mneg{}(x  =  y)@i'
\mvdash{}  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    P[L[j];L[i]]


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((BackThruSomeHyp  THEN  Auto')))

---

Home Index