---

Step * of Lemma equiv-bijection-property

∀A,B:Type. ∀e:{() ⊢ _:Equiv(discr(A);discr(B))}.  Bij(A;B;equiv-bijection(e))
BY
{ (Intros THEN UseWitness ⌜equiv-bijection-is(e)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}e:\{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}.    Bij(A;B;equiv-bijection(e))


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}equiv-bijection-is(e)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index