---

Step * of Lemma exception-name_wf

∀[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].  (exception-name(t;n) ∈ 𝔹)
BY
{ Auto }

1
1. n : Atom2
2. t : Value() ⋃ Exception(n;Top)
⊢ exception-name(t;n) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}[n:Atom2].  \mforall{}[t:Value()  \mcup{}  Exception(n;Top)].    (exception-name(t;n)  \mmember{}  \mBbbB{})


By

---

Latex:
Auto

---

Home Index