---

Step * of Lemma discrete-equiv-iff

∀A,B:Type.  ({() ⊢ _:Equiv(discr(A);discr(B))} ⇐⇒ A ~ B)
BY
{ Auto }

1
1. A : Type
2. B : Type
3. {() ⊢ _:Equiv(discr(A);discr(B))}
⊢ A ~ B

2
1. A : Type
2. B : Type
3. A ~ B
⊢ {() ⊢ _:Equiv(discr(A);discr(B))}

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (\{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  B)


By

---

Latex:
Auto

---

Home Index