---

Step * of Lemma binrel_eqv_functionality_wrt_breqv

∀[T:Type]. ∀[a,a',b,b':T ⟶ T ⟶ ℙ].  ((a <≡>{T} b) ⇒ (a' <≡>{T} b') ⇒ (a <≡>{T} a' ⇐⇒ b <≡>{T} b'))
BY
{ ((D 0 THENM BLemma `uequiv_rel_self_functionality`) THENA Auto)⋅ }

1
1. [T] : Type
⊢ UniformEquivRel(T ⟶ T ⟶ ℙ;x,y.x <≡>{T} y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,a',b,b':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((a  <\mequiv{}>\{T\}  b)  {}\mRightarrow{}  (a'  <\mequiv{}>\{T\}  b')  {}\mRightarrow{}  (a  <\mequiv{}>\{T\}  a'  \mLeftarrow{}{}\mRightarrow{}  b  <\mequiv{}>\{T\}  b'))


By

---

Latex:
((D  0  THENM  BLemma  `uequiv\_rel\_self\_functionality`)  THENA  Auto)\mcdot{}

---

Home Index