---

Step * of Lemma subst-frame_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List].  (subst-frame(s;t) ∈ term(opr))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[s:(varname()  \mtimes{}  term(opr))  List].    (subst-frame(s;t)  \mmember{}  term(opr))


By

---

Latex:
ProveWfLemma

---

Home Index