---

Step * 2 1 1 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. aaaa : a:A × b:A × (R a b)
6. LLLL : (a:A × b:A × (R a b)) List
7. ∀x,y,z:A. ∀r:R y z.  rel_path(A;LLLL @ [<y, z, r>];x;z) supposing rel_path(A;LLLL;x;y)
8. x : A
9. y : A
10. z : A
11. r : R y z
12. [%2] : rel_path(A;[aaaa / LLLL];x;y)
⊢ SqStable(rel_path(A;[aaaa / LLLL] @ [<y, z, r>];x;z))
BY
{ ((InstLemma `sq_stable__rel_path` [⌜A⌝;⌜R⌝]⋅ THENA Auto) THEN BHyp -1 THEN 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.  aaaa  :  a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b)
6.  LLLL  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
7.  \mforall{}x,y,z:A.  \mforall{}r:R  y  z.    rel\_path(A;LLLL  @  [<y,  z,  r>];x;z)  supposing  rel\_path(A;LLLL;x;y)
8.  x  :  A
9.  y  :  A
10.  z  :  A
11.  r  :  R  y  z
12.  [\%2]  :  rel\_path(A;[aaaa  /  LLLL];x;y)
\mvdash{}  SqStable(rel\_path(A;[aaaa  /  LLLL]  @  [<y,  z,  r>];x;z))


By

---

Latex:
((InstLemma  `sq\_stable\_\_rel\_path`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1  THEN  Auto)

---

Home Index