---

Step * 3 of Lemma rel_path-append


1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. L : (a:A × b:A × (R a b)) List
4. ∀[x,y:A]. ∀[L:(a:A × b:A × (R a b)) List].  (rel_path(A;L;x;y) ∈ ℙ)
5. ∀L:(a:A × b:A × (R a b)) List. ∀x,y,z:A. ∀r:R y z.  rel_path(A;L @ [<y, z, r>];x;z) supposing rel_path(A;L;x;y)
⊢ ∀x,y,z:A. ∀r:R y z.  rel_path(A;L @ [<y, z, r>];x;z) supposing rel_path(A;L;x;y)
BY
{ Auto }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  L  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
4.  \mforall{}[x,y:A].  \mforall{}[L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List].    (rel\_path(A;L;x;y)  \mmember{}  \mBbbP{})
5.  \mforall{}L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List.  \mforall{}x,y,z:A.  \mforall{}r:R  y  z.
          rel\_path(A;L  @  [<y,  z,  r>];x;z)  supposing  rel\_path(A;L;x;y)
\mvdash{}  \mforall{}x,y,z:A.  \mforall{}r:R  y  z.    rel\_path(A;L  @  [<y,  z,  r>];x;z)  supposing  rel\_path(A;L;x;y)


By

---

Latex:
Auto

---

Home Index