---

Step * of Lemma ml_match_nil_wf

∀[T:Type]. ∀[e:Top List]. ∀[t:T].  (ml_match_nil(e;t) ∈ 𝔹 × T)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[e:Top  List].  \mforall{}[t:T].    (ml\_match\_nil(e;t)  \mmember{}  \mBbbB{}  \mtimes{}  T)


By

---

Latex:
ProveWfLemma

---

Home Index