---

Step * 1 1 of Lemma last_index_property


1. T : Type
2. P : T ⟶ 𝔹
3. (↑P[⊥]) ∧ (¬(∃x∈[]. ↑P[x])) supposing 0 < 0
4. 0 = 0 ∈ ℤ
⊢ ¬(∃x∈[]. ↑P[x])
BY
{ TACTIC:((D 0 THEN Auto) THEN D -1 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  (\muparrow{}P[\mbot{}])  \mwedge{}  (\mneg{}(\mexists{}x\mmember{}[].  \muparrow{}P[x]))  supposing  0  <  0
4.  0  =  0
\mvdash{}  \mneg{}(\mexists{}x\mmember{}[].  \muparrow{}P[x])


By

---

Latex:
TACTIC:((D  0  THEN  Auto)  THEN  D  -1  THEN  Auto')

---

Home Index