---

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

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

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

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

---

Latex:

---

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


By

---

Latex:
Subst'  tt  \msim{}  n  0

---

Home Index