---

Step * 1 of Lemma discrete-equiv-iff


1. A : Type
2. B : Type
3. {() ⊢ _:Equiv(discr(A);discr(B))}
⊢ A ~ B
BY
{ (RenameVar `e' (-1) THEN UseWitness ⌜<equiv-bijection(e), equiv-bijection-is(e)>⌝⋅) }

1
1. A : Type
2. B : Type
3. e : {() ⊢ _:Equiv(discr(A);discr(B))}
⊢ <equiv-bijection(e), equiv-bijection-is(e)> ∈ A ~ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}
\mvdash{}  A  \msim{}  B


By

---

Latex:
(RenameVar  `e'  (-1)  THEN  UseWitness  \mkleeneopen{}<equiv-bijection(e),  equiv-bijection-is(e)>\mkleeneclose{}\mcdot{})

---

Home Index