---

Step * of Lemma quotient-squash

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T//E[x;y] ≡ x,y:T//(↓E[x;y]) supposing EquivRel(T;x,y.E[x;y])
BY
{ (Auto
   THEN (FLemma `equiv_rel_squash` [-1] THENA Auto)
   THEN D 0
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN SqExRepD
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    x,y:T//E[x;y]  \mequiv{}  x,y:T//(\mdownarrow{}E[x;y])  supposing  EquivRel(T;x,y.E[x;y])


By

---

Latex:
(Auto
  THEN  (FLemma  `equiv\_rel\_squash`  [-1]  THENA  Auto)
  THEN  D  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  SqExRepD
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index