---

Step * of Lemma equiv-bijection_wf

∀[A,B:Type]. ∀[e:{() ⊢ _:Equiv(discr(A);discr(B))}].  (equiv-bijection(e) ∈ A ⟶ B)
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index