---

Step * of Lemma tagged-test_wf

∀[T:Type]. ∀[x:"b":𝔹 |+ "a":ℤ].  (tagged-test(x) ∈ "b":𝔹 |+ "a":ℤ)
BY
{ xxxxxxxxxxxxProveWfLemmaxxxxxxxxxxxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:"b":\mBbbB{}  |+  "a":\mBbbZ{}].    (tagged-test(x)  \mmember{}  "b":\mBbbB{}  |+  "a":\mBbbZ{})


By

---

Latex:
xxxxxxxxxxxxProveWfLemmaxxxxxxxxxxxx

---

Home Index