---

Step * of Lemma rel_star_functionality_wrt_rel_implies

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1^* => R2^*)
BY
{ ((InstLemma `rel_star_monotonic` [] THEN Auto) THEN Unfold `rel_implies` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  rel\_star(T;  R1)  =>  rel\_star(T;  R2))


By

---

Latex:
((InstLemma  `rel\_star\_monotonic`  []  THEN  Auto)  THEN  Unfold  `rel\_implies`  0  THEN  Auto)

---

Home Index