---

Step * 1 2 2 1 of Lemma no-excluded-middle-quot-true


1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : Base
3. v2 : Base
4. v = v2 ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
5. v ∈ (⊥)↓ ∨ (↓¬(⊥)↓)
6. v2 ∈ (⊥)↓ ∨ (↓¬(⊥)↓)
7. True
8. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
9. v1 : Base
10. v3 : Base
11. v1 = v3 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
12. v1 ∈ (0 ≤ 0) ∨ (↓¬(0 ≤ 0))
13. v3 ∈ (0 ≤ 0) ∨ (↓¬(0 ≤ 0))
14. True
15. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
16. y : ↓¬(⊥)↓
17. v = (inr y ) ∈ ((⊥)↓ ∨ (↓¬(⊥)↓))
18. x : 0 ≤ 0
19. v1 = (inl x) ∈ ((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ λx.Ax ∈ ¬(λx.x ≤ ⊥)
BY
{ (Auto THEN InstLemma `not_id_sqeq_bottom` [] THEN D (-1) THEN SqequalSqle THEN Auto) }

---

Latex:

---

Latex:

1.  magic  :  \mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mdownarrow{}\mneg{}P))
2.  v  :  Base
3.  v2  :  Base
4.  v  =  v2
5.  v  \mmember{}  (\mbot{})\mdownarrow{}  \mvee{}  (\mdownarrow{}\mneg{}(\mbot{})\mdownarrow{})
6.  v2  \mmember{}  (\mbot{})\mdownarrow{}  \mvee{}  (\mdownarrow{}\mneg{}(\mbot{})\mdownarrow{})
7.  True
8.  (magic  (\mbot{})\mdownarrow{})  =  v
9.  v1  :  Base
10.  v3  :  Base
11.  v1  =  v3
12.  v1  \mmember{}  (0  \mleq{}  0)  \mvee{}  (\mdownarrow{}\mneg{}(0  \mleq{}  0))
13.  v3  \mmember{}  (0  \mleq{}  0)  \mvee{}  (\mdownarrow{}\mneg{}(0  \mleq{}  0))
14.  True
15.  (magic  (0  \mleq{}  0))  =  v1
16.  y  :  \mdownarrow{}\mneg{}(\mbot{})\mdownarrow{}
17.  v  =  (inr  y  )
18.  x  :  0  \mleq{}  0
19.  v1  =  (inl  x)
\mvdash{}  \mlambda{}x.Ax  \mmember{}  \mneg{}(\mlambda{}x.x  \mleq{}  \mbot{})


By

---

Latex:
(Auto  THEN  InstLemma  `not\_id\_sqeq\_bottom`  []  THEN  D  (-1)  THEN  SqequalSqle  THEN  Auto)

---

Home Index