---

Step * of Lemma rel_star_weakening

∀[T:Type]. ∀[x,y:T]. ∀[R:T ⟶ T ⟶ ℙ].  x (R^*) y supposing x = y ∈ T
BY
{ ((((((Auto THEN Unfold `rel_star` 0) THEN Reduce 0) THEN InstConcl [0]) THEN Auto) THEN ReduceExp 0) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((((((Auto  THEN  Unfold  `rel\_star`  0)  THEN  Reduce  0)  THEN  InstConcl  [0])  THEN  Auto)  THEN  ReduceExp  0)
  THEN  Auto
  )

---

Home Index