---

Step * 1 of Lemma rel-path-between-append


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. L1 : T List
4. L2 : T List
5. x : T
6. y : T
7. z : T
8. rel-path-between(T;R;x;y;L1)
9. rel-path-between(T;R;y;z;L2)
10. Refl(T;v1,v2.R v1 v2)
⊢ rel-path-between(T;R;x;z;L1 @ L2)
BY
{ (All (RepUR ``rel-path-between``) THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. L1 : T List
4. L2 : T List
5. x : T
6. y : T
7. z : T
8. rel-path(R;L1)
9. 0 < ||L1||
10. x = hd(L1) ∈ T
11. y = last(L1) ∈ T
12. rel-path(R;L2)
13. 0 < ||L2||
14. y = hd(L2) ∈ T
15. z = last(L2) ∈ T
16. Refl(T;v1,v2.R v1 v2)
⊢ rel-path(R;L1 @ L2)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  L1  :  T  List
4.  L2  :  T  List
5.  x  :  T
6.  y  :  T
7.  z  :  T
8.  rel-path-between(T;R;x;y;L1)
9.  rel-path-between(T;R;y;z;L2)
10.  Refl(T;v1,v2.R  v1  v2)
\mvdash{}  rel-path-between(T;R;x;z;L1  @  L2)


By

---

Latex:
(All  (RepUR  ``rel-path-between``)  THEN  Auto)

---

Home Index