---

Step * 1 of Lemma bl-exists-first


1. [A] : Type
2. P : A ⟶ 𝔹
⊢ (∃x∈[]. ↑P[x]) ⇐⇒ ∃i:ℕ0. ((↑P[⊥]) ∧ (∀j:ℕi. (¬↑P[⊥])))
BY
{ (Auto THEN Try (Complete ((ExRepD THEN D (-3) THEN Auto))) THEN Try (Complete ((RW ListC (-1) THEN Auto)))) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  (\mexists{}x\mmember{}[].  \muparrow{}P[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}0.  ((\muparrow{}P[\mbot{}])  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}P[\mbot{}])))


By

---

Latex:
(Auto
  THEN  Try  (Complete  ((ExRepD  THEN  D  (-3)  THEN  Auto)))
  THEN  Try  (Complete  ((RW  ListC  (-1)  THEN  Auto))))

---

Home Index