---

Step * of Lemma decidable__quotient_equal

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y]) ⇒ (∀x,y:T.  Dec(E[x;y])) ⇒ (∀u,v:x,y:T//E[x;y].  Dec(u = v ∈ (x,y:T//E[x;y]))))
BY
{ RepeatFor 4 (D 0 THENA Auto)⋅ }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. ∀x,y:T.  Dec(E[x;y])
⊢ ∀u,v:x,y:T//E[x;y].  Dec(u = v ∈ (x,y:T//E[x;y]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(E[x;y]))  {}\mRightarrow{}  (\mforall{}u,v:x,y:T//E[x;y].    Dec(u  =  v)))


By

---

Latex:
RepeatFor  4  (D  0  THENA  Auto)\mcdot{}

---

Home Index