---

Step * 1 1 1 1 1 1 of Lemma decidable__quotient_equal


1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. f : T ⟶ T ⟶ 𝔹
5. ∀x,y:T.  (↑(x f y) ⇐⇒ E[x;y])
6. u : T
7. u1 : T
8. E[u;u1]
9. v : x,y:T//E[x;y]
⊢ f u v = f u1 v
BY
{ (quotD (-1) THEN Auto) }

1
1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. f : T ⟶ T ⟶ 𝔹
5. ∀x,y:T.  (↑(x f y) ⇐⇒ E[x;y])
6. u : T
7. u1 : T
8. E[u;u1]
9. v : T
10. v1 : T
11. E[v;v1]
⊢ f u v = f u1 v1

---

Latex:

---

Latex:

1.  T  :  Type
2.  E  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}x,y:T.    (\muparrow{}(x  f  y)  \mLeftarrow{}{}\mRightarrow{}  E[x;y])
6.  u  :  T
7.  u1  :  T
8.  E[u;u1]
9.  v  :  x,y:T//E[x;y]
\mvdash{}  f  u  v  =  f  u1  v


By

---

Latex:
(quotD  (-1)  THEN  Auto)

---

Home Index