---

Step * of Lemma exists-union

∀[A,B:Type].  ∀P:(A + B) ⟶ ℙ. (∃x:A + B. P[x] ⇐⇒ (∃a:A. P[inl a]) ∨ (∃b:B. P[inr b ]))
BY
{ (Auto
   THEN SplitOrHyps
   THEN ExRepD
   THEN Try ((With ⌜inl a⌝ (D 0)⋅ THEN Auto))
   THEN Try ((With ⌜inr b ⌝ (D 0)⋅ THEN Auto))
   THEN D -2
   THEN Try ((OrLeft THEN Complete (Auto)))
   THEN Try ((OrRight THEN Complete (Auto)))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  Try  ((With  \mkleeneopen{}inl  a\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  Try  ((With  \mkleeneopen{}inr  b  \mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  D  -2
  THEN  Try  ((OrLeft  THEN  Complete  (Auto)))
  THEN  Try  ((OrRight  THEN  Complete  (Auto))))

---

Home Index