---

Step * 3 1 of Lemma pairwise-cons


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
9. ¬(j = 0 ∈ ℤ)
⊢ P[[x / L][j];L[i - 1]]
BY
{ (RWO "select-cons-tl" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T@i
3.  L  :  T  List@i
4.  [P]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}'
5.  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    P[L[j];L[i]]@i'
6.  (\mforall{}y\mmember{}L.P[x;y])@i'
7.  i  :  \mBbbN{}||[x  /  L]||@i
8.  j  :  \mBbbN{}i@i
9.  \mneg{}(j  =  0)
\mvdash{}  P[[x  /  L][j];L[i  -  1]]


By

---

Latex:
(RWO  "select-cons-tl"  0  THEN  Auto)

---

Home Index