---

Step * of Lemma uall-union

∀[A,B:Type].  ∀P:(A + B) ⟶ ℙ. ((∀[x:A + B]. P[x]) ⇒ ((∀[a:A]. P[inl a]) ∧ (∀[b:B]. P[inr b ])))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}P:(A  +  B)  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}[x:A  +  B].  P[x])  {}\mRightarrow{}  ((\mforall{}[a:A].  P[inl  a])  \mwedge{}  (\mforall{}[b:B].  P[inr  b  ])))


By

---

Latex:
Auto

---

Home Index