---

Step * of Lemma rel_star_of_equiv

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (EquivRel(T)(_1 E _2) ⇒ (x (E^*) y) ⇒ (x E y))
BY
{ (((Unfold `rel_star` 0 THEN Reduce 0) THEN Auto) THEN ExRepD) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. EquivRel(T)(_1 E _2)
6. n : ℕ
7. x E^n y
⊢ x E y

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    (EquivRel(T)($_{1}$  E  $_{2\mbackslash{}ff\000C7d$)  {}\mRightarrow{}  (x  rel\_star(T;  E)  y)  {}\mRightarrow{}  (x  E  y))


By

---

Latex:
(((Unfold  `rel\_star`  0  THEN  Reduce  0)  THEN  Auto)  THEN  ExRepD)

---

Home Index