---

Step * of Lemma rel-connected_weakening

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y:T].  x──R⟶y supposing x = y ∈ T
BY
{ (Unfold `rel-connected` 0
   THEN Auto
   THEN RepUR ``rel_star infix_ap`` 0
   THEN With 0 (D 0)⋅
   THEN Auto
   THEN RecUnfold `rel_exp` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x,y:T].    x{}{}R{}\mrightarrow{}y  supposing  x  =  y


By

---

Latex:
(Unfold  `rel-connected`  0
  THEN  Auto
  THEN  RepUR  ``rel\_star  infix\_ap``  0
  THEN  With  0  (D  0)\mcdot{}
  THEN  Auto
  THEN  RecUnfold  `rel\_exp`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index