---

Step * 2 3 2 1 2 of Lemma rel-path-between-cons


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. u : T
4. v : T List
5. ¬([u / v] = [] ∈ (T List))
6. x : T
7. y : T
8. z : T
9. x = z ∈ T
10. y = z ∈ T supposing False
11. x R u
12. ∀i:ℕ(||v|| + 1) - 1. ([u / v][i] R [u / v][i + 1])
13. 0 < ||v|| + 1
14. u = u ∈ T
15. y = last([u / v]) ∈ T
16. i : ℕ((||v|| + 1) + 1) - 1
17. ¬(i = 0 ∈ ℤ)
⊢ [z; [u / v]][i] R [z; [u / v]][i + 1]
BY
{ (RWO "select_cons_tl" 0 THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  u  :  T
4.  v  :  T  List
5.  \mneg{}([u  /  v]  =  [])
6.  x  :  T
7.  y  :  T
8.  z  :  T
9.  x  =  z
10.  y  =  z  supposing  False
11.  x  R  u
12.  \mforall{}i:\mBbbN{}(||v||  +  1)  -  1.  ([u  /  v][i]  R  [u  /  v][i  +  1])
13.  0  <  ||v||  +  1
14.  u  =  u
15.  y  =  last([u  /  v])
16.  i  :  \mBbbN{}((||v||  +  1)  +  1)  -  1
17.  \mneg{}(i  =  0)
\mvdash{}  [z;  [u  /  v]][i]  R  [z;  [u  /  v]][i  +  1]


By

---

Latex:
(RWO  "select\_cons\_tl"  0  THEN  Auto')\mcdot{}

---

Home Index