---

Step * 1 of Lemma binrel_eqv_functionality_wrt_breqv


1. [T] : Type
⊢ UniformEquivRel(T ⟶ T ⟶ ℙ;x,y.x <≡>{T} y)
BY
{ ((AGenRepD ["basic";"compound"]) THENA Auto) }

1
1. [T] : Type
2. [a] : T ⟶ T ⟶ ℙ
⊢ a <≡>{T} a

2
1. [T] : Type
2. [a] : T ⟶ T ⟶ ℙ
3. [b] : T ⟶ T ⟶ ℙ
4. a <≡>{T} b@i
⊢ b <≡>{T} a

3
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

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  UniformEquivRel(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{};x,y.x  <\mequiv{}>\{T\}  y)


By

---

Latex:
((AGenRepD  ["basic";"compound"])  THENA  Auto)

---

Home Index