---

Step * of Lemma inl-one-one'

No Annotations
∀[A,B:Type]. ∀[x,y:A].  x = y ∈ A supposing (inl x) = (inl y) ∈ (A + B)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[x,y:A].    x  =  y  supposing  (inl  x)  =  (inl  y)


By

---

Latex:
Auto

---

Home Index