---

Step * of Lemma process-valueall-type

∀[M,E:Type ⟶ Type].  valueall-type(process(P.M[P];P.E[P])) supposing M[Top]
BY
{ (Auto THEN InstLemma `subtype-valueall-type` [⌜process(P.M[P];P.E[P])⌝;⌜M[Top] ⟶ (Top × E[Top])⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. M : Type ⟶ Type
2. E : Type ⟶ Type
3. M[Top]
⊢ process(P.M[P];P.E[P]) ⊆r (M[Top] ⟶ (Top × E[Top]))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  InstLemma  `subtype-valueall-type`  [\mkleeneopen{}process(P.M[P];P.E[P])\mkleeneclose{};\mkleeneopen{}M[Top]  {}\mrightarrow{}  (Top  \mtimes{}  E[Top])\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index