---

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


1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
3. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
4. v1 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
5. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ ¬(case v of inl(a) => ⊥ | inr(b) => λx.x ≤ case v1 of inl(a) => ⊥ | inr(b) => λx.x)
BY
{ (UseWitness ⌜λx.Ax⌝⋅ THEN OnVar `v' (QuotientElimForEqualityAux Id)⋅) }

1
.....wf..... 
1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
3. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
4. v1 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
5. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ ¬(case v of inl(a) => ⊥ | inr(b) => λ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 : ⇃((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))

3
.....aux..... 
1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : Base
3. v2 : Base
4. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
5. v1 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
6. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ istype((v ∈ (⊥)↓ ∨ (↓¬(⊥)↓)) ∧ (v2 ∈ (⊥)↓ ∨ (↓¬(⊥)↓)) ∧ True)

---

Latex:

---

Latex:

1.  magic  :  \mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mdownarrow{}\mneg{}P))
2.  v  :  \00D9((\mbot{})\mdownarrow{}  \mvee{}  (\mdownarrow{}\mneg{}(\mbot{})\mdownarrow{}))
3.  (magic  (\mbot{})\mdownarrow{})  =  v
4.  v1  :  \00D9((0  \mleq{}  0)  \mvee{}  (\mdownarrow{}\mneg{}(0  \mleq{}  0)))
5.  (magic  (0  \mleq{}  0))  =  v1
\mvdash{}  \mneg{}(case  v  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x  \mleq{}  case  v1  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x)


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}\mcdot{}  THEN  OnVar  `v'  (QuotientElimForEqualityAux  Id)\mcdot{})

---

Home Index