---

Step * of Lemma rel-immediate_functionality_wrt_breqv

∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  ((R <≡>{T} Q) ⇒ (R! <≡>{T} Q!))
BY
{ (Unfold `binrel_eqv` 0 THEN InstLemma `rel-immediate_functionality_wrt_iff` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,Q:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R  <\mequiv{}>\{T\}  Q)  {}\mRightarrow{}  (R!  <\mequiv{}>\{T\}  Q!))


By

---

Latex:
(Unfold  `binrel\_eqv`  0  THEN  InstLemma  `rel-immediate\_functionality\_wrt\_iff`  []  THEN  Trivial)

---

Home Index