---

Step * 1 1 1 2 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. f ∈ (x,y:T//E[x;y]) ⟶ (x,y:T//E[x;y]) ⟶ 𝔹
7. u : x,y:T//E[x;y]
8. v : x,y:T//E[x;y]
⊢ ↓↑(u f v) ⇐⇒ u = v ∈ (x,y:T//E[x;y])
BY
{ (UseEqWitness ⌜Ax⌝
   THEN (OnVar `u' quotD THEN Auto THEN Repeat ((EqCD THEN Auto)))
   THEN OnVar `v' quotD
   THEN Auto
   THEN Repeat ((EqCD 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. f ∈ (x,y:T//E[x;y]) ⟶ (x,y:T//E[x;y]) ⟶ 𝔹
7. u : T
8. u1 : T
9. E[u;u1]
10. v : T
11. v1 : T
12. E[v;v1]
⊢ Ax ∈ ↓↑(u f v) ⇐⇒ u = v ∈ (x,y:T//E[x;y])

---

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.  f  \mmember{}  (x,y:T//E[x;y])  {}\mrightarrow{}  (x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbB{}
7.  u  :  x,y:T//E[x;y]
8.  v  :  x,y:T//E[x;y]
\mvdash{}  \mdownarrow{}\muparrow{}(u  f  v)  \mLeftarrow{}{}\mRightarrow{}  u  =  v


By

---

Latex:
(UseEqWitness  \mkleeneopen{}Ax\mkleeneclose{}
  THEN  (OnVar  `u'  quotD  THEN  Auto  THEN  Repeat  ((EqCD  THEN  Auto)))
  THEN  OnVar  `v'  quotD
  THEN  Auto
  THEN  Repeat  ((EqCD  THEN  Auto)))

---

Home Index