---

Step * of Lemma rel_exp0

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R^0 y ⇐⇒ x = y ∈ T)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    (x  rel\_exp(T;  R;  0)  y  \mLeftarrow{}{}\mRightarrow{}  x  =  y)


By

---

Latex:
Auto

---

Home Index