---

Step * 2 1 of Lemma free-from-atom-bool-subtype

.....assertion..... 
1. a : Atom1
2. T : Type
3. T ⊆r 𝔹
4. n : T
5. b : 𝔹
6. ¬↑b
7. n = ff
⊢ ff ∈ T
BY
{ Subst' ff ~ n 0 }

1
.....equality..... 
1. a : Atom1
2. T : Type
3. T ⊆r 𝔹
4. n : T
5. b : 𝔹
6. ¬↑b
7. n = ff
⊢ ff ~ n

2
1. a : Atom1
2. T : Type
3. T ⊆r 𝔹
4. n : T
5. b : 𝔹
6. ¬↑b
7. n = ff
⊢ n ∈ T

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  Atom1
2.  T  :  Type
3.  T  \msubseteq{}r  \mBbbB{}
4.  n  :  T
5.  b  :  \mBbbB{}
6.  \mneg{}\muparrow{}b
7.  n  =  ff
\mvdash{}  ff  \mmember{}  T


By

---

Latex:
Subst'  ff  \msim{}  n  0

---

Home Index