---

Step * 1 3 of Lemma binrel_eqv_functionality_wrt_breqv


1. [T] : Type
2. [a] : T ⟶ T ⟶ ℙ
3. [b] : T ⟶ T ⟶ ℙ
4. [c] : T ⟶ T ⟶ ℙ
5. a <≡>{T} b@i
6. b <≡>{T} c@i
⊢ a <≡>{T} c
BY
{ ((FLemma `binrel_eqv_transitivity` [5;6]) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [a]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [b]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  [c]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  a  <\mequiv{}>\{T\}  b@i
6.  b  <\mequiv{}>\{T\}  c@i
\mvdash{}  a  <\mequiv{}>\{T\}  c


By

---

Latex:
((FLemma  `binrel\_eqv\_transitivity`  [5;6])  THEN  Auto)

---

Home Index