---

Step * of Lemma rel_exp_functionality_wrt_brle

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

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R1  \mequiv{}>\{T\}  R2)  {}\mRightarrow{}  (R1\^{}n  \mequiv{}>\{T\}  R2\^{}n))


By

---

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

---

Home Index