---

Step * of Lemma rel-path-between-append

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀L1,L2:T List. ∀x,y,z:T.
    (rel-path-between(T;R;x;y;L1)
    ⇒ rel-path-between(T;R;y;z;L2)
    ⇒ Refl(T;v1,v2.R v1 v2)
    ⇒ rel-path-between(T;R;x;z;L1 @ L2))
BY
{ 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-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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L1,L2:T  List.  \mforall{}x,y,z:T.
        (rel-path-between(T;R;x;y;L1)
        {}\mRightarrow{}  rel-path-between(T;R;y;z;L2)
        {}\mRightarrow{}  Refl(T;v1,v2.R  v1  v2)
        {}\mRightarrow{}  rel-path-between(T;R;x;z;L1  @  L2))


By

---

Latex:
Auto

---

Home Index