---

Step * of Lemma inl-inr-disjoint

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index