---

Step * of Lemma equipollent-quotient2

∀[A:Type]
  ∀E:A ⟶ A ⟶ ℙ. ∀d:∀x,y:A.  Dec(↓E[x;y]).
    A ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)}  supposing EquivRel(A;x,y.↓E[x;y])
BY
{ (Auto
   THEN (Assert ∀x,y:A.  (isl(d x y) ∈ 𝔹) BY
               (Auto THEN GenConclTerm ⌜d x y⌝⋅ THEN Auto))
   THEN (Assert ∀x,y:A.  (↑isl(d x y) ⇐⇒ ↓E[x;y]) BY
               ((UnivCD THENA Auto) THEN (GenConclTerm ⌜d x y⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto))
   THEN (InstLemma `equipollent-quotient` [⌜A⌝;⌜λ2x y.isl(d x y)⌝]⋅ THENA (Auto THEN RWO  "-1" 0 THEN Auto))) }

1
1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A.  Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A.  (isl(d x y) ∈ 𝔹)
6. ∀x,y:A.  (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} 
⊢ A ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} 

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}d:\mforall{}x,y:A.    Dec(\mdownarrow{}E[x;y]).
        A  \msim{}  a:x,y:A//(\mdownarrow{}E[x;y])  \mtimes{}  \{b:A|  \muparrow{}isl(d  a  b)\}    supposing  EquivRel(A;x,y.\mdownarrow{}E[x;y])


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}x,y:A.    (isl(d  x  y)  \mmember{}  \mBbbB{})  BY
                          (Auto  THEN  GenConclTerm  \mkleeneopen{}d  x  y\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}x,y:A.    (\muparrow{}isl(d  x  y)  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}E[x;y])  BY
                          ((UnivCD  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}d  x  y\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (InstLemma  `equipollent-quotient`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.isl(d  x  y)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RWO    "-1"  0  THEN  Auto)
              ))

---

Home Index