---

Step * of Lemma respects-equality-quotient1

∀[X,T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (respects-equality(X;x,y:T//E[x;y])) supposing (respects-equality(X;T) and EquivRel(T;x,y.E[x;y]))
BY
{ (Intros THEN RepeatFor 4 ((D 0 THENA Auto))) }

1
1. X : Type
2. T : Type
3. E : T ⟶ T ⟶ ℙ
4. EquivRel(T;x,y.E[x;y])
5. respects-equality(X;T)
6. x : Base
7. y : Base
8. x = y ∈ X
9. x ∈ x,y:T//E[x;y]
⊢ x = y ∈ (x,y:T//E[x;y])

---

Latex:

---

Latex:
\mforall{}[X,T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (respects-equality(X;x,y:T//E[x;y]))  supposing  (respects-equality(X;T)  and  EquivRel(T;x,y.E[x;y]))


By

---

Latex:
(Intros  THEN  RepeatFor  4  ((D  0  THENA  Auto)))

---

Home Index