---

Step * of Lemma equipollent-decidable-equal

∀[A,B:Type].  (A ~ B ⇒ (∀x,y:B.  Dec(x = y ∈ B)) ⇒ {∀x,y:A.  Dec(x = y ∈ A)})
BY
{ (Unfolds ``equipollent guard`` 0 THEN Auto THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B@i
4. Bij(A;B;f)@i
5. ∀x,y:B.  Dec(x = y ∈ B)@i
6. x : A@i
7. y : A@i
⊢ Dec(x = y ∈ A)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (A  \msim{}  B  {}\mRightarrow{}  (\mforall{}x,y:B.    Dec(x  =  y))  {}\mRightarrow{}  \{\mforall{}x,y:A.    Dec(x  =  y)\})


By

---

Latex:
(Unfolds  ``equipollent  guard``  0  THEN  Auto  THEN  ExRepD)

---

Home Index