---

Step * of Lemma rel_star_symmetric

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Sym(T;x,y.x R y) ⇒ Sym(T;x,y.x (R^*) y))
BY
{ ((Unfold `sym` 0 THEN Reduce 0) THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀a,b:T.  ((a R b) ⇒ (b R a))
4. a : T
5. b : T
6. a (R^*) b
⊢ b (R^*) a

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (Sym(T;x,y.x  R  y)  {}\mRightarrow{}  Sym(T;x,y.x  rel\_star(T;  R)  y))


By

---

Latex:
((Unfold  `sym`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index