---

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

∀[a:Atom1]. ∀[T:Type].  ∀[n:T]. a#n:T supposing T ⊆r 𝔹
BY
{ ((Auto THEN GenConcl ⌜n = b⌝⋅) THEN Auto THEN AutoBoolCase ⌜b⌝⋅) }

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

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

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[T:Type].    \mforall{}[n:T].  a\#n:T  supposing  T  \msubseteq{}r  \mBbbB{}


By

---

Latex:
((Auto  THEN  GenConcl  \mkleeneopen{}n  =  b\mkleeneclose{}\mcdot{})  THEN  Auto  THEN  AutoBoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{})

---

Home Index