---

Step * of Lemma pairwise-cons

∀[T:Type]. ∀x:T. ∀L:T List.  ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈[x / L].  P[x;y]) ⇐⇒ (∀x,y∈L.  P[x;y]) ∧ (∀y∈L.P[x;y]))
BY
{ (Auto THEN (All (Unfold `pairwise`)) THEN Auto) }

1
1. [T] : Type
2. x : T@i
3. L : T List@i
4. [P] : T ⟶ T ⟶ ℙ'
5. ∀i:ℕ||[x / L]||. ∀j:ℕi.  P[[x / L][j];[x / L][i]]@i'
6. i : ℕ||L||@i
7. j : ℕi@i
⊢ P[L[j];L[i]]

2
1. [T] : Type
2. x : T@i
3. L : T List@i
4. [P] : T ⟶ T ⟶ ℙ'
5. ∀i:ℕ||[x / L]||. ∀j:ℕi.  P[[x / L][j];[x / L][i]]@i'
⊢ (∀y∈L.P[x;y])

3
1. [T] : Type
2. x : T@i
3. L : T List@i
4. [P] : T ⟶ T ⟶ ℙ'
5. ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]@i'
6. (∀y∈L.P[x;y])@i'
7. i : ℕ||[x / L]||@i
8. j : ℕi@i
⊢ P[[x / L][j];[x / L][i]]

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (All  (Unfold  `pairwise`))  THEN  Auto)

---

Home Index