---

Step * 3 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
⊢ P[[x / L][j];[x / L][i]]
BY
{ (CaseNat 0 `j'
   THEN Reduce 0
   THEN (Subst ⌜i ~ (i - 1) + 1⌝ 0⋅ THENL [(Assert ⌜i ∈ ℤ⌝⋅ THEN Auto); Id])
   THEN RWO "select_cons_tl_sq" 0
   THEN Auto') }

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

---

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
\mvdash{}  P[[x  /  L][j];[x  /  L][i]]


By

---

Latex:
(CaseNat  0  `j'
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}i  \msim{}  (i  -  1)  +  1\mkleeneclose{}  0\mcdot{}  THENL  [(Assert  \mkleeneopen{}i  \mmember{}  \mBbbZ{}\mkleeneclose{}\mcdot{}  THEN  Auto);  Id])
  THEN  RWO  "select\_cons\_tl\_sq"  0
  THEN  Auto')

---

Home Index