Step
*
of Lemma
subst-term_wf
No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List].  (subst-term(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-term(s;t)  \mmember{}  term(opr))
By
Latex:
ProveWfLemma
Home
Index