---

Step * of Lemma inr-inl-disjoint

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index