---

Step * of Lemma inl-one-one

∀[A,B:Type]. ∀[x,y:A].  uiff((inl x) = (inl y) ∈ (A + B);x = y ∈ A)
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[x,y:A].    uiff((inl  x)  =  (inl  y);x  =  y)


By

---

Latex:
xxxAutoxxx

---

Home Index