---

Step * of Lemma no-repeats-pairwise

∀[T:Type]
  ∀L:T List
    ∀[P:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ']
      (∀x,y:{x:T| (x ∈ L)} .  P[x;y] supposing ¬(x = y ∈ T)) ⇒ (∀x,y∈L.  P[x;y]) supposing no_repeats(T;L)
BY
{ (Auto THEN Unfold `pairwise` 0 THEN Unfold `no_repeats` -2) }

1
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]]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}']
            (\mforall{}x,y:\{x:T|  (x  \mmember{}  L)\}  .    P[x;y]  supposing  \mneg{}(x  =  y))  {}\mRightarrow{}  (\mforall{}x,y\mmember{}L.    P[x;y]) 
            supposing  no\_repeats(T;L)


By

---

Latex:
(Auto  THEN  Unfold  `pairwise`  0  THEN  Unfold  `no\_repeats`  -2)

---

Home Index