---

Step * 1 2 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 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
10. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ (λx.Ax) = (λx.Ax) ∈ (¬(case v of inl(a) => ⊥ | inr(b) => λx.x ≤ case v1 of inl(a) => ⊥ | inr(b) => λx.x))
BY
{ ((GenConcl ⌜v = w ∈ ((⊥)↓ ∨ (↓¬(⊥)↓))⌝⋅ THENA Auto)
   THEN D -2
   THEN Try (BotDiv)
   THEN Reduce 0
   THEN Fold `member` 0
   THEN OnVar `v1' (QuotientElimForEqualityAux Id)) }

1
.....wf..... 
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 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
10. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
11. y : ↓¬(⊥)↓
12. v = (inr y ) ∈ ((⊥)↓ ∨ (↓¬(⊥)↓))
⊢ ¬(λx.x ≤ case v1 of inl(a) => ⊥ | inr(b) => λx.x) ∈ Type

2
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 ) ∈ ((⊥)↓ ∨ (↓¬(⊥)↓))
⊢ (λx.Ax) = (λx.Ax) ∈ (¬(λx.x ≤ case v1 of inl(a) => ⊥ | inr(b) => λx.x))

3
.....aux..... 
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. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
12. y : ↓¬(⊥)↓
13. v = (inr y ) ∈ ((⊥)↓ ∨ (↓¬(⊥)↓))
⊢ istype((v1 ∈ (0 ≤ 0) ∨ (↓¬(0 ≤ 0))) ∧ (v3 ∈ (0 ≤ 0) ∨ (↓¬(0 ≤ 0))) ∧ True)

---

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  :  \00D9((0  \mleq{}  0)  \mvee{}  (\mdownarrow{}\mneg{}(0  \mleq{}  0)))
10.  (magic  (0  \mleq{}  0))  =  v1
\mvdash{}  (\mlambda{}x.Ax)  =  (\mlambda{}x.Ax)


By

---

Latex:
((GenConcl  \mkleeneopen{}v  =  w\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Try  (BotDiv)
  THEN  Reduce  0
  THEN  Fold  `member`  0
  THEN  OnVar  `v1'  (QuotientElimForEqualityAux  Id))

---

Home Index