---

Step * of Lemma sq_stable__rel_path

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀L:(a:A × b:A × (R a b)) List. ∀[x,y:A].  SqStable(rel_path(A;L;x;y))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN Unfold `rel_path` 0 THEN ListInd (-1)⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List.  \mforall{}[x,y:A].    SqStable(rel\_path(A;L;x;y))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  Unfold  `rel\_path`  0  THEN  ListInd  (-1)\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index