---

Step * of Lemma prefix-replace_wf

∀[t,x:Name]. ∀[pre:pi_prefix()].  (prefix-replace(t;x;pre) ∈ pi_prefix())
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[t,x:Name].  \mforall{}[pre:pi\_prefix()].    (prefix-replace(t;x;pre)  \mmember{}  pi\_prefix())


By

---

Latex:
ProveWfLemma

---

Home Index