---

Step * of Lemma pairwise-implies

∀[T:Type]
  ∀L:T List
    ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L.  P[x;y]) ⇒ (∀x,y:T.  ((x ∈ L) ⇒ (y ∈ L) ⇒ ((x = y ∈ T) ∨ P[x;y] ∨ P[y;x]))))
BY
{ (Unfolds ``pairwise l_member`` 0
   THEN Auto
   THEN ExRepD
   THEN (HypSubst (-4) 0 THEN Auto)
   THEN HypSubst (-1) 0
   THEN Auto) }

1
1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ'
4. ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]
5. x : T
6. y : T
7. i1 : ℕ
8. i1 < ||L||
9. x = L[i1] ∈ T
10. i : ℕ
11. i < ||L||
12. y = L[i] ∈ T
⊢ (L[i1] = L[i] ∈ T) ∨ P[L[i1];L[i]] ∨ P[L[i];L[i1]]

---

Latex:

---

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


By

---

Latex:
(Unfolds  ``pairwise  l\_member``  0
  THEN  Auto
  THEN  ExRepD
  THEN  (HypSubst  (-4)  0  THEN  Auto)
  THEN  HypSubst  (-1)  0
  THEN  Auto)

---

Home Index