---

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


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

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

---

Latex:

---

Latex:

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{}  a\#ff:T


By

---

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

---

Home Index