---

Step * of Lemma equiv-equipollent-implies-quotient-equipollent

∀[A,B:Type].  ∀E:A ⟶ A ⟶ ℙ. A ~ B mod (a1,a2.E[a1;a2]) ⇒ x,y:A//E[x;y] ~ B supposing EquivRel(A;x,y.E[x;y])
BY
{ (Auto
   THEN (Assert x,y:A//E[x;y] ~ x,y:A//(↓E[x;y]) BY
               (BLemma `equipollent_weakening_ext-eq` THEN EAuto 1))
   THEN (Assert EquivRel(A;x,y.↓E[x;y]) BY
               (Unhide
                THEN EAuto 1
                THEN (D 0 THEN Auto)
                THEN RepeatFor 2 ((D 0 THEN Auto))
                THEN D 0
                THEN Auto
                THEN UseTrans ⌜b⌝⋅))) }

1
1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. A ~ B mod (a1,a2.E[a1;a2])
6. x,y:A//E[x;y] ~ x,y:A//(↓E[x;y])
7. EquivRel(A;x,y.↓E[x;y])
⊢ x,y:A//E[x;y] ~ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  A  \msim{}  B  mod  (a1,a2.E[a1;a2])  {}\mRightarrow{}  x,y:A//E[x;y]  \msim{}  B  supposing  EquivRel(A;x,y.E[x;y])


By

---

Latex:
(Auto
  THEN  (Assert  x,y:A//E[x;y]  \msim{}  x,y:A//(\mdownarrow{}E[x;y])  BY
                          (BLemma  `equipollent\_weakening\_ext-eq`  THEN  EAuto  1))
  THEN  (Assert  EquivRel(A;x,y.\mdownarrow{}E[x;y])  BY
                          (Unhide
                            THEN  EAuto  1
                            THEN  (D  0  THEN  Auto)
                            THEN  RepeatFor  2  ((D  0  THEN  Auto))
                            THEN  D  0
                            THEN  Auto
                            THEN  UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{})))

---

Home Index