---

Step * of Lemma test-rel-connected

∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀x,y,z,w:T.  ((x (R^*) y) ⇒ (y = z ∈ T) ⇒ (z (R^*) w) ⇒ (x (R^*) w))
BY
{ Auto }

1
1. T : Type@i'
2. R : T ⟶ T ⟶ ℙ@i'
3. x : T@i
4. y : T@i
5. z : T@i
6. w : T@i
7. x (R^*) y@i
8. y = z ∈ T@i
9. z (R^*) w@i
⊢ x (R^*) w

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x,y,z,w:T.
    ((x  (R\^{}*)  y)  {}\mRightarrow{}  (y  =  z)  {}\mRightarrow{}  (z  (R\^{}*)  w)  {}\mRightarrow{}  (x  rel\_star(T;  R)  w))


By

---

Latex:
Auto

---

Home Index