---

Step * of Lemma rel_star_monotonic

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (R1 => R2 ⇒ (x (R1^*) y) ⇒ (x (R2^*) y))
BY
{ ((((Auto THEN AssertBY R1^* => R2^*        (BackThruLemma `rel_star_monotone` THEN Auto))
     THEN Unfold `rel_implies` (-1)
     )
    THEN BackThruHyp (-1)
    )
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:T.    (R1  =>  R2  {}\mRightarrow{}  (x  (R1\^{}*)  y)  {}\mRightarrow{}  (x  (R2\^{}*)  y))


By

---

Latex:
((((Auto  THEN  AssertBY  R1\^{}*  =>  R2\^{}*              (BackThruLemma  `rel\_star\_monotone`  THEN  Auto))
      THEN  Unfold  `rel\_implies`  (-1)
      )
    THEN  BackThruHyp  (-1)
    )
  THEN  Auto
  )

---

Home Index