---

Step * of Lemma process-value-type

∀[M,E:Type ─→ Type].  value-type(process(P.M[P];P.E[P])) supposing M[Top]
BY
{ EAuto 1 }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].    value-type(process(P.M[P];P.E[P]))  supposing  M[Top]


By

EAuto  1

---

Home Index