---

Step * 2 of Lemma squash-list-exists


1. A : Type
2. B : Type
3. R : A ⟶ B ⟶ ℙ
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (↓∃b:B. R[v[i];b])) ⇒ (↓∃bs:B List. ((||bs|| = ||v|| ∈ ℤ) ∧ (∀i:ℕ||v||. R[v[i];bs[i]])))
7. ∀i:ℕ||v|| + 1. (↓∃b:B. R[[u / v][i];b])
⊢ ↓∃bs:B List. ((||bs|| = (||v|| + 1) ∈ ℤ) ∧ (∀i:ℕ||v|| + 1. R[[u / v][i];bs[i]]))
BY
{ ((D (-2) THENA (Auto THEN With ⌜i + 1⌝ (D (-2))⋅ THEN Auto))
   THEN (InstHyp [⌜0⌝] (-2)⋅ THENA Auto)
   THEN SqExRepD
   THEN All Reduce
   THEN D 0
   THEN With ⌜[b / bs]⌝ (D 0)⋅
   THEN Auto) }

1
1. A : Type
2. B : Type
3. R : A ⟶ B ⟶ ℙ
4. u : A
5. v : A List
6. ∀i:ℕ||v|| + 1. (↓∃b:B. R[[u / v][i];b])
7. bs : B List
8. ||bs|| = ||v|| ∈ ℤ
9. ∀i:ℕ||v||. R[v[i];bs[i]]
10. b : B
11. R[u;b]
12. ||[b / bs]|| = (||v|| + 1) ∈ ℤ
13. i : ℕ||v|| + 1
⊢ R[[u / v][i];[b / bs][i]]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  R  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
4.  u  :  A
5.  v  :  A  List
6.  (\mforall{}i:\mBbbN{}||v||.  (\mdownarrow{}\mexists{}b:B.  R[v[i];b]))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}bs:B  List.  ((||bs||  =  ||v||)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  R[v[i];bs[i]])))
7.  \mforall{}i:\mBbbN{}||v||  +  1.  (\mdownarrow{}\mexists{}b:B.  R[[u  /  v][i];b])
\mvdash{}  \mdownarrow{}\mexists{}bs:B  List.  ((||bs||  =  (||v||  +  1))  \mwedge{}  (\mforall{}i:\mBbbN{}||v||  +  1.  R[[u  /  v][i];bs[i]]))


By

---

Latex:
((D  (-2)  THENA  (Auto  THEN  With  \mkleeneopen{}i  +  1\mkleeneclose{}  (D  (-2))\mcdot{}  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  SqExRepD
  THEN  All  Reduce
  THEN  D  0
  THEN  With  \mkleeneopen{}[b  /  bs]\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index