---

Step * of Lemma rel_star_functionality_wrt_brle

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 ≡>{T} R2) ⇒ ((R1^*) ≡>{T} (R2^*)))
BY
{ (InstLemma `rel_star_functionality_wrt_rel_implies` []
   THEN RepUR ``rel_implies infix_ap`` -1
   THEN Fold `binrel_le` (-1)
   THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rel\_star\_functionality\_wrt\_rel\_implies`  []
  THEN  RepUR  ``rel\_implies  infix\_ap``  -1
  THEN  Fold  `binrel\_le`  (-1)
  THEN  Trivial)

---

Home Index