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