---

Step * of Lemma simple-bind-nxt_wf

∀[A,B,C:Type]. ∀[Y:B ⟶ hdataflow(A;C)]. ∀[p:hdataflow(A;B) × bag(hdataflow(A;C))]. ∀[a:A].
  simple-bind-nxt(Y; p; a) ∈ hdataflow(A;B) × bag(hdataflow(A;C)) × bag(C) supposing valueall-type(C)
BY
{ ProveWfLemmaAux (Try (Complete Auto)) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[p:hdataflow(A;B)  \mtimes{}  bag(hdataflow(A;C))].  \mforall{}[a:A].
    simple-bind-nxt(Y;  p;  a)  \mmember{}  hdataflow(A;B)  \mtimes{}  bag(hdataflow(A;C))  \mtimes{}  bag(C) 
    supposing  valueall-type(C)


By

---

Latex:
ProveWfLemmaAux  (Try  (Complete  Auto))

---

Home Index