---

Step * of Lemma rel_exp_functionality_wrt_rel_implies

∀n:ℕ. ∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1^n => R2^n)
BY
{ (InstLemma `rel_exp_monotone` [] THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rel\_exp\_monotone`  []  THEN  Trivial)

---

Home Index