---

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


1. a : Atom1
2. T : Type
3. T ⊆r 𝔹
4. n : T
5. b : 𝔹
6. n = b
7. ↑b
⊢ a#tt:T
BY
{ (Assert ⌜tt ∈ T⌝⋅ THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}tt  \mmember{}  T\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index